{-# 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-GY8B (pt : propositional-truncations-exist) (fe : Fun-Ext) (pe : propext 𝓤) (ρ : propositional-resizing (𝓤 ⁺) 𝓤) where open Conjunction open Universal fe open Implication fe
Proposition 1.2 的左伴隨 L 定義為
L(f)(p) = ∀q. (((p → q) ∧ (f q → q)) → q)
但因為類型論的關係，它落在 Ω (𝓤 ⁺)
上（L⁺）
L⁺ : (Ω 𝓤 → Ω 𝓤) → Ω 𝓤 → Ω (𝓤 ⁺) L⁺ f p = Ɐ q ꞉ Ω 𝓤 , ((p ⇒ q) ∧ (f q ⇒ q)) ⇒ q
論文裡 Ω 是 impredicative，全稱量化後仍落在
Ω；所以要靠 propositional resizing 把它放回去
Ω 𝓤 得到 L
L : (Ω 𝓤 → Ω 𝓤) → Ω 𝓤 → Ω 𝓤 L f p = resize ρ (L⁺ f p holds) (holds-is-prop (L⁺ f p)) , resize-is-prop ρ (L⁺ f p holds) (holds-is-prop (L⁺ f p))
ηL、εL 是在兩種 size
之間搬動證明的轉換器。讀法上，(L⁺ f p) holds 展開後就是
(q : Ω 𝓤) → (p ⇒ q) holds × (f q ⇒ q) holds → q holds
後面所有證明都先用 εL 把 L f p 拆成上面的
universal property、再用 ηL 把證明包回去。
ηL : (f : Ω 𝓤 → Ω 𝓤) (p : Ω 𝓤) → (L⁺ f p) holds → (L f p) holds ηL f p = to-resize ρ (L⁺ f p holds) (holds-is-prop (L⁺ f p)) εL : (f : Ω 𝓤 → Ω 𝓤) (p : Ω 𝓤) → (L f p) holds → (L⁺ f p) holds εL f p = from-resize ρ (L⁺ f p holds) (holds-is-prop (L⁺ f p))