{-# 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-XCL4
  (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-UAEO pt fe pe ρ
open import ag-GY8B pt fe pe ρ
open import ag-GK6B pt fe pe ρ
open is-local-operator

(→) 對任意 local operator j，若 f ≼ j 則 L f ≼ j，在 L f p 裡代入 q := j p

L-adjunction-→ :
  (m : Mon) {j : Ω 𝓤 → Ω 𝓤} → is-local-operator j
  → (monotone-function m ≼ j) holds → (L (monotone-function m) ≼ j) holds
L-adjunction-→ (f , _) {j} j-is-local-op f≼j p L[f][p] = εL f p L[f][p] (j p) (p⇒jp , fjp⇒jp)
  where
  p⇒jp : (p ⇒ j p) holds
  p⇒jp = LO-infl j-is-local-op p

  fjp⇒jp : (f (j p) ⇒ j p) holds
  fjp⇒jp x = idem j-is-local-op p (f≼j (j p) x)

(←)：伴隨的單位是 f ≼ L f，要用到 f 的單調性。

f≼Lf : ((f , f-is-monotone) : Mon) → (f ≼ L f) holds
f≼Lf (f , f-is-monotone) p f[p] = ηL f p I
  where
  I : (L⁺ f p) holds
  I q (p⇒q , fq⇒q) = fq⇒q f[q]
    where
    f[q] : f q holds
    f[q] = f-is-monotone p q p⇒q f[p]

L-adjunction-← : (m : Mon) {j : Ω 𝓤 → Ω 𝓤} → is-local-operator j
              → (L (monotone-function m) ≼ j) holds → (monotone-function m ≼ j) holds
L-adjunction-← m {j} j-is-local-op Lf≼j p fp = Lf≼j p (f≼Lf m p fp)