{-# OPTIONS --safe --without-K #-}
open import MLTT.Spartan
open import UF.FunExt
open import UF.PropTrunc
open import UF.Subsingletons
open import UF.SubtypeClassifier
open import UF.Size
open import UF.Logic

module ag-95LU
  (pt : propositional-truncations-exist)
  (fe : Fun-Ext)
  (pe : propext 𝓤)
  (ρ  : propositional-resizing (𝓤 ⁺) 𝓤)
  where

open Conjunction
open Universal   fe
open Implication fe

open import ag-V2O7 pt fe pe ρ
open import ag-5W9X pt fe pe ρ
open import ag-GY8B pt fe pe ρ
open is-local-operator

L-is-local-operator : (m : Mon) → is-local-operator (L (monotone-function m))

每個欄位對應 local operator 的一個條件，每個都需要「εL 拆開 → 操作 → ηL 包裝」

(i) 單調：給定 p ⇒ q，把目標裡的 q ⇒ r 沿著 p ⇒ q 前接成 p ⇒ r，再餵回 L f p

L-is-local-operator (f , fm) .mono p q p⇒q lfp = ηL f q goal
  where
  goal : (L⁺ f q) holds
  goal r (q⇒r , fr⇒r) = εL f p lfp r (p⇒r , fr⇒r)
    where
    p⇒r : (p ⇒ r) holds
    p⇒r p = q⇒r (p⇒q p)

(ii) ⊤ ⇒ L f ⊤：此時 q 直接由 ⊤ ⇒ q 得到

L-is-local-operator (f , fm) .unit _ = ηL f ⊤ goal
  where
  goal : (L⁺ f ⊤) holds
  goal q (⊤⇒q , fq⇒q) = ⊤⇒q ⊤-holds

(iii) 冪等 L f (L f p) ⇒ L f p：在外層代入 q := L f p。關鍵的小引理 f (L f p) ⇒ L f p 正好用到 f 的單調性

L-is-local-operator (f , f-is-monotone) .idem p ll =
  εL f (L f p) ll (L f p) (id-L , f∘L⇒Lf)
  where
  id-L : (L f p ⇒ L f p) holds
  id-L x = x

  f∘L⇒Lf : (f (L f p) ⇒ L f p) holds
  f∘L⇒Lf f[L[f[p]]] = ηL f p I
    where
    I : (L⁺ f p) holds
    I q (p⇒q , fq⇒q) = fq⇒q f[q]
      where
      -- 把 (p ⇒ q), (f q ⇒ q) 餵給 L f p
      Lfp⇒q : (L f p ⇒ q) holds
      Lfp⇒q L[f[p]] = εL f p L[f[p]] q (p⇒q , fq⇒q)

      -- f 單調表示 L f p ⇒ q 可以變成 f (L f p) ⇒ f q
      f[q] : f q holds
      f[q] = f-is-monotone (L f p) q Lfp⇒q f[L[f[p]]]