Local operator 跟 Nucleus 有什麼關聯？
{-# OPTIONS --safe --without-K #-} open import MLTT.Spartan open import UF.Base open import UF.Equiv open import UF.FunExt open import UF.PropTrunc open import UF.Subsingletons open import UF.SubtypeClassifier open import UF.SubtypeClassifier-Properties open import UF.Size open import UF.Logic open import UF.Subsingletons-FunExt open import UF.EquivalenceExamples module ag-X72H (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 import ag-95LU pt fe pe ρ open import ag-GK6B pt fe pe ρ open import ag-3HBW pt fe pe ρ open is-local-operator
Ω 𝓤 本身就是一個 frame（the initial frame
𝟎-𝔽𝕣𝕞）
Ω 𝓤- order 是
⇒ - meet 是
∧
於是 Nucleus Ωᶠ 正好可與 is-local-operator
對照
open import Locales.Frame pt fe open import Locales.InitialFrame pt fe open import Locales.Sublocale.Nucleus pt fe Ωᶠ : Frame (𝓤 ⁺) 𝓤 𝓤 Ωᶠ = 𝟎-𝔽𝕣𝕞 pe
Nucleus 的 inflationary + idempotent + meet-preserving 可以推得 local
operator 的 monotone + unit + idempotent，單調性由
nuclei-are-monotone 提供
nucleus-to-local-operator : (n : Nucleus Ωᶠ) → is-local-operator (pr₁ n) nucleus-to-local-operator n@(j , inf , idm , _) .mono p q p⇒q = nuclei-are-monotone Ωᶠ n (p , q) p⇒q nucleus-to-local-operator n@(j , inf , idm , _) .unit = inf ⊤ nucleus-to-local-operator n@(j , inf , idm , _) .idem p = idm p
local operator 可以推得 Nucleus
local-operator-to-nucleus : (j : Ω 𝓤 → Ω 𝓤) → is-local-operator j → Nucleus Ωᶠ local-operator-to-nucleus j j-is-local-op = j , inflationary , idempotent , meet-preserving where inflationary : is-inflationary Ωᶠ j holds inflationary x = LO-infl j-is-local-op x idempotent : is-idempotent Ωᶠ j holds idempotent x = idem j-is-local-op x I : (p : Ω 𝓤) → L j p ＝ j p I p = Ω-extensionality pe fe ⇒-dir ⇐-dir where ⇒-dir : (L j p ⇒ j p) holds ⇒-dir ljp = εL j p ljp (j p) (inflationary p , idempotent p) ⇐-dir : (j p ⇒ L j p) holds ⇐-dir jp = ηL j p II where II : (L⁺ j p) holds II q (p⇒q , jq⇒q) = jq⇒q (mono j-is-local-op p q p⇒q jp) is-meet-preserving : (Ω 𝓤 → Ω 𝓤) → 𝓤 ⁺ ̇ is-meet-preserving j = (p q : Ω 𝓤) → j (p ∧ q) ＝ j p ∧ j q meet-preserving : is-meet-preserving j meet-preserving p q = j (p ∧ q) ＝⟨ (I (p ∧ q)) ⁻¹ ⟩ L j (p ∧ q) ＝⟨ L-preserves-arg-∧ (j , j-is-local-op .mono) p q ⟩ L j p ∧ L j q ＝⟨ ap₂ _∧_ (I p) (I q) ⟩ j p ∧ j q ∎
所以從 monotone 也可以得到 Nucleus
L-nucleus : (m : Mon) → Nucleus Ωᶠ L-nucleus m = local-operator-to-nucleus (L (monotone-function m)) (L-is-local-operator m)
is-local-operator 也是 proposition
is-local-operator-is-prop : (j : Ω 𝓤 → Ω 𝓤) → is-prop (is-local-operator j) is-local-operator-is-prop j = equiv-to-prop unfold Fields-is-prop where Fields : 𝓤 ⁺ ̇ Fields = is-monotone j holds × (⊤ {𝓤} ⇒ j ⊤) holds × ((p : Ω 𝓤) → (j (j p) ⇒ j p) holds) unfold : is-local-operator j ≃ Fields unfold = qinveq (λ r → mono r , unit r , idem r) ( (λ (m , u , i) → record { mono = m ; unit = u ; idem = i }) , (λ _ → refl) , (λ _ → refl) ) Fields-is-prop : is-prop Fields Fields-is-prop = ×-is-prop (holds-is-prop (is-monotone j)) (×-is-prop (holds-is-prop (⊤ {𝓤} ⇒ j ⊤)) (Π-is-prop fe (λ p → holds-is-prop (j (j p) ⇒ j p))))
型別 Loc 與 Nucleus Ωᶠ 等價
Loc : 𝓤 ⁺ ̇ Loc = Σ j ꞉ (Ω 𝓤 → Ω 𝓤) , is-local-operator j Loc-≃-Nucleus : Loc ≃ Nucleus Ωᶠ Loc-≃-Nucleus = Σ-cong predicates-agree where predicates-agree : (j : Ω 𝓤 → Ω 𝓤) → is-local-operator j ≃ is-nucleus Ωᶠ j holds predicates-agree j = logically-equivalent-props-are-equivalent (is-local-operator-is-prop j) (holds-is-prop (is-nucleus Ωᶠ j)) ([⇒]) ([⇐]) where [⇒] : is-local-operator j → is-nucleus Ωᶠ j holds [⇒] j-lo = pr₂ (local-operator-to-nucleus j j-lo) [⇐] : is-nucleus Ωᶠ j holds → is-local-operator j [⇐] n = nucleus-to-local-operator (j , n)