diff --git a/README.md b/README.md index b07dfa2..bfe5f56 100644 --- a/README.md +++ b/README.md @@ -36,8 +36,8 @@ This is a formalization of the displacement algebras, their properties, and part | :------------------------------------ | :----------------- | :----------------------------------------------------------------------------------------------- | | Validity of McBride monads | 3.1 | [McBride](./src/Mugen/Cat/HierarchyTheory/McBride.agda) | | Embedding of endomorphisms | 3.4 (Lemma 3.8) | [EndomorphismEmbedding](./src/Mugen/Cat/HierarchyTheory/Universality/EndomorphismEmbedding.agda) | -| Embedding of small hierarchy theories | 3.4 (Lemma 3.9) | _(TODO)_ | -| Universality of McBride monads | 3.4 (Theorem 3.10) | _(TODO)_ | +| Embedding of small hierarchy theories | 3.4 (Lemma 3.9) | [SubcategoryEmbedding](./src/Mugen/Cat/HierarchyTheory/Universality/SubcategoryEmbedding.agda) | +| Universality of McBride monads | 3.4 (Theorem 3.10) | [Universality](./src/Mugen/Cat/HierarchyTheory/Universality.agda) | ## Building diff --git a/src/Mugen/Cat/HierarchyTheory/Universality.agda b/src/Mugen/Cat/HierarchyTheory/Universality.agda new file mode 100644 index 0000000..682e1c8 --- /dev/null +++ b/src/Mugen/Cat/HierarchyTheory/Universality.agda @@ -0,0 +1,137 @@ +-- vim: nowrap +open import Order.Instances.Discrete +open import Order.Instances.Coproduct + +open import Cat.Prelude +open import Cat.Functor.Base +open import Cat.Functor.Compose +open import Cat.Functor.Properties +open import Cat.Diagram.Monad + +import Cat.Reasoning as Cat +import Cat.Functor.Reasoning as FR + +open import Mugen.Prelude + +open import Mugen.Algebra.Displacement +open import Mugen.Algebra.Displacement.Instances.Endomorphism + +open import Mugen.Cat.Endomorphisms +open import Mugen.Cat.Indexed +open import Mugen.Cat.StrictOrders +open import Mugen.Cat.Monad +open import Mugen.Cat.HierarchyTheory +open import Mugen.Cat.HierarchyTheory.McBride + +open import Mugen.Order.StrictOrder +open import Mugen.Order.Instances.Endomorphism renaming (Endomorphism to Endomorphism-poset) +open import Mugen.Order.Instances.LeftInvariantRightCentered +open import Mugen.Order.Instances.Lift +open import Mugen.Order.Instances.Singleton + +import Mugen.Order.Reasoning as Reasoning + +-------------------------------------------------------------------------------- +-- The Universal Embedding Theorem +-- Section 3.4, Theorem 3.10 + +module Mugen.Cat.HierarchyTheory.Universality {o o' r} + (H : Hierarchy-theory (o ⊔ o') (r ⊔ o')) {I : Type o'} ⦃ Discrete-I : Discrete I ⦄ + (Δ₋ : ⌞ I ⌟ → Poset (o ⊔ o') (r ⊔ o')) (Ψ : Set (lsuc (o ⊔ r ⊔ o'))) where + + private + import Mugen.Cat.HierarchyTheory.Universality.SubcategoryEmbedding as SubcategoryEmbedding + module SE = SubcategoryEmbedding {o = o} {r = r} H Δ₋ + + import Mugen.Cat.HierarchyTheory.Universality.EndomorphismEmbedding as EndomorphismEmbedding + module EE = EndomorphismEmbedding H SE.Δ Ψ + + import Mugen.Cat.HierarchyTheory.Universality.EndomorphismEmbeddingNaturality as EndomorphismEmbeddingNaturality + module EEN = EndomorphismEmbeddingNaturality H SE.Δ Ψ + + -------------------------------------------------------------------------------- + -- Notation + + private + open Strictly-monotone + open Algebra-hom + module H = Monad H + + SOrd : Precategory (lsuc (o ⊔ r ⊔ o')) (o ⊔ r ⊔ o') + SOrd = Strict-orders (o ⊔ o') (r ⊔ o') + open Cat SOrd + + SOrdᴴ : Precategory (lsuc (o ⊔ r ⊔ o')) (lsuc (o ⊔ r ⊔ o')) + SOrdᴴ = Eilenberg-Moore SOrd H + module SOrdᴴ = Cat SOrdᴴ + + -- '↑' for lifting + SOrd↑ : Precategory (lsuc (lsuc (o ⊔ r ⊔ o'))) (lsuc (o ⊔ r ⊔ o')) + SOrd↑ = Strict-orders (lsuc (o ⊔ r ⊔ o')) (lsuc (o ⊔ r ⊔ o')) + module SOrd↑ = Cat SOrd↑ + + SOrdᴹᴰ : Precategory (lsuc (lsuc (o ⊔ r ⊔ o'))) (lsuc (lsuc (o ⊔ r ⊔ o'))) + SOrdᴹᴰ = Eilenberg-Moore SOrd↑ (McBride (Endomorphism H EE.Δ⁺)) + module SOrdᴹᴰ = Cat SOrdᴹᴰ + + Uᴴ : Functor SOrdᴴ SOrd + Uᴴ = Forget SOrd H + + Fᴴ : Functor SOrd SOrdᴴ + Fᴴ = Free SOrd H + + Fᴴ₀ : Poset (o ⊔ o') (r ⊔ o') → Algebra SOrd H + Fᴴ₀ = Fᴴ .Functor.F₀ + + Fᴴ₁ : {X Y : Poset (o ⊔ o') (r ⊔ o')} → Hom X Y → SOrdᴴ.Hom (Fᴴ₀ X) (Fᴴ₀ Y) + Fᴴ₁ = Fᴴ .Functor.F₁ + + Fᴹᴰ : Functor SOrd↑ SOrdᴹᴰ + Fᴹᴰ = Free SOrd↑ (McBride (Endomorphism H EE.Δ⁺)) + + Fᴹᴰ₀ : Poset (lsuc (o ⊔ r ⊔ o')) (lsuc (o ⊔ r ⊔ o')) → Algebra SOrd↑ (McBride (Endomorphism H EE.Δ⁺)) + Fᴹᴰ₀ = Fᴹᴰ .Functor.F₀ + + Uᴹᴰ : Functor SOrdᴹᴰ SOrd↑ + Uᴹᴰ = Forget SOrd↑ (McBride (Endomorphism H EE.Δ⁺)) + + -------------------------------------------------------------------------------- + -- Constructing the natural transformation T + -- Section 3.4, Theorem 3.10 + + T : Functor (Indexed SOrdᴴ λ i → Fᴴ₀ (Δ₋ i)) (Endos SOrdᴹᴰ (Fᴹᴰ₀ (Disc Ψ))) + T = EE.T F∘ SE.T + + -------------------------------------------------------------------------------- + -- Constructing the natural transformation ν + -- Section 3.4, Theorem 3.10 + + ν : ∣ Ψ ∣ + → liftᶠ-strict-orders F∘ Uᴴ F∘ Indexed-include + => Uᴹᴰ F∘ Endos-include F∘ T + ν pt = lemma-assoc₂ + ∘nt (EEN.ν pt ◂ SE.T) + ∘nt lemma-assoc₁ + ∘nt (liftᶠ-strict-orders ▸ SE.ν) + where + lemma-assoc₁ + : liftᶠ-strict-orders F∘ Uᴴ F∘ Endos-include F∘ SE.T + => (liftᶠ-strict-orders F∘ Uᴴ F∘ Endos-include) F∘ SE.T + lemma-assoc₁ ._=>_.η _ = SOrd↑.id + lemma-assoc₁ ._=>_.is-natural _ _ _ = SOrd↑.id-comm-sym + + lemma-assoc₂ + : (Uᴹᴰ F∘ Endos-include F∘ EE.T) F∘ SE.T + => Uᴹᴰ F∘ Endos-include F∘ EE.T F∘ SE.T + lemma-assoc₂ ._=>_.η _ = SOrd↑.id + lemma-assoc₂ ._=>_.is-natural _ _ _ = SOrd↑.id-comm-sym + + -------------------------------------------------------------------------------- + -- Faithfulness of T + -- Section 3.4, Lemma 3.9 + + abstract + T-faithful : ∣ Ψ ∣ → preserves-monos H → is-faithful T + T-faithful pt H-preserves-monos eq = + SE.T-faithful H-preserves-monos $ + EE.T-faithful pt H-preserves-monos eq diff --git a/src/Mugen/Cat/HierarchyTheory/Universality/EndomorphismEmbedding.agda b/src/Mugen/Cat/HierarchyTheory/Universality/EndomorphismEmbedding.agda index 6c2497d..70df921 100644 --- a/src/Mugen/Cat/HierarchyTheory/Universality/EndomorphismEmbedding.agda +++ b/src/Mugen/Cat/HierarchyTheory/Universality/EndomorphismEmbedding.agda @@ -53,21 +53,24 @@ module Mugen.Cat.HierarchyTheory.Universality.EndomorphismEmbedding module Δ = Poset Δ module H = Monad H - Δ⁺ : Poset o r - Δ⁺ = ◆ {o = o} {r = r} ⊎ᵖ (Δ ⊎ᵖ Δ) + -- made public for the naturality proof in a different file + Δ⁺ : Poset o r + Δ⁺ = ◆ {o = o} {r = r} ⊎ᵖ (Δ ⊎ᵖ Δ) + private H⟨Δ⁺⟩ : Poset o r H⟨Δ⁺⟩ = H.M₀ Δ⁺ module H⟨Δ⁺⟩ = Reasoning H⟨Δ⁺⟩ - H⟨Δ⁺⟩→-poset : Poset (lsuc (o ⊔ r)) (o ⊔ r) - H⟨Δ⁺⟩→-poset = Endomorphism-poset H Δ⁺ - module H⟨Δ⁺⟩→-poset = Reasoning H⟨Δ⁺⟩→-poset + H⟨Δ⁺⟩→ : Poset (lsuc (o ⊔ r)) (o ⊔ r) + H⟨Δ⁺⟩→ = Endomorphism-poset H Δ⁺ + module H⟨Δ⁺⟩→ = Reasoning H⟨Δ⁺⟩→ - H⟨Δ⁺⟩→ : Displacement-on H⟨Δ⁺⟩→-poset - H⟨Δ⁺⟩→ = Endomorphism H Δ⁺ - module H⟨Δ⁺⟩→ = Displacement-on H⟨Δ⁺⟩→ + 𝒟 : Displacement-on H⟨Δ⁺⟩→ + 𝒟 = Endomorphism H Δ⁺ + module 𝒟 = Displacement-on 𝒟 + private SOrd : Precategory (lsuc (o ⊔ r)) (o ⊔ r) SOrd = Strict-orders o r module SOrd = Cat SOrd @@ -81,7 +84,7 @@ module Mugen.Cat.HierarchyTheory.Universality.EndomorphismEmbedding SOrd↑ = Strict-orders (lsuc (o ⊔ r)) (lsuc (o ⊔ r)) SOrdᴹᴰ : Precategory (lsuc (lsuc (o ⊔ r))) (lsuc (lsuc (o ⊔ r))) - SOrdᴹᴰ = Eilenberg-Moore SOrd↑ (McBride H⟨Δ⁺⟩→) + SOrdᴹᴰ = Eilenberg-Moore SOrd↑ (McBride 𝒟) module SOrdᴹᴰ = Cat SOrdᴹᴰ Fᴴ : Functor SOrd SOrdᴴ @@ -96,8 +99,8 @@ module Mugen.Cat.HierarchyTheory.Universality.EndomorphismEmbedding Endoᴴ⟨Δ⟩ : Type (o ⊔ r) Endoᴴ⟨Δ⟩ = Hom (H.M₀ Δ) (H.M₀ Δ) - Fᴹᴰ₀ : Poset (lsuc o ⊔ lsuc r) (lsuc o ⊔ lsuc r) → Algebra SOrd↑ (McBride H⟨Δ⁺⟩→) - Fᴹᴰ₀ = Functor.F₀ (Free SOrd↑ (McBride H⟨Δ⁺⟩→)) + Fᴹᴰ₀ : Poset (lsuc o ⊔ lsuc r) (lsuc o ⊔ lsuc r) → Algebra SOrd↑ (McBride 𝒟) + Fᴹᴰ₀ = Functor.F₀ (Free SOrd↑ (McBride 𝒟)) -- These patterns and definitions are exported for the naturality proof -- in another file. @@ -186,7 +189,7 @@ module Mugen.Cat.HierarchyTheory.Universality.EndomorphismEmbedding T .Functor.F₀ _ = tt T .Functor.F₁ σ .morphism .hom (α , d) = α , (T′ σ SOrdᴴ.∘ d) T .Functor.F₁ σ .morphism .pres-≤[]-equal {α , d1} {β , d2} p = - let d1≤d2 , injr = H⟨Δ⁺⟩→.left-strict-invariant {T′ σ} {d1} {d2} (⋉-snd-invariant p) in + let d1≤d2 , injr = 𝒟.left-strict-invariant {T′ σ} {d1} {d2} (⋉-snd-invariant p) in inc (biased (⋉-fst-invariant p) d1≤d2) , λ q i → q i .fst , injr (ap snd q) i T .Functor.F₁ σ .commutes = trivial! T .Functor.F-id = ext λ α d → diff --git a/src/Mugen/Cat/HierarchyTheory/Universality/EndomorphismEmbeddingNaturality.agda b/src/Mugen/Cat/HierarchyTheory/Universality/EndomorphismEmbeddingNaturality.agda index 7dcce5f..2d0c131 100644 --- a/src/Mugen/Cat/HierarchyTheory/Universality/EndomorphismEmbeddingNaturality.agda +++ b/src/Mugen/Cat/HierarchyTheory/Universality/EndomorphismEmbeddingNaturality.agda @@ -57,9 +57,6 @@ module Mugen.Cat.HierarchyTheory.Universality.EndomorphismEmbeddingNaturality module Δ = Poset Δ module H = Monad H - Δ⁺ : Poset o r - Δ⁺ = ◆ {o = o} {r = r} ⊎ᵖ (Δ ⊎ᵖ Δ) - H⟨Δ⟩ : Poset o r H⟨Δ⟩ = H.M₀ Δ module H⟨Δ⟩ = Poset H⟨Δ⟩ @@ -68,13 +65,9 @@ module Mugen.Cat.HierarchyTheory.Universality.EndomorphismEmbeddingNaturality H⟨Δ⁺⟩ = H.M₀ Δ⁺ module H⟨Δ⁺⟩ = Reasoning H⟨Δ⁺⟩ - H⟨Δ⁺⟩→-poset : Poset (lsuc (o ⊔ r)) (o ⊔ r) - H⟨Δ⁺⟩→-poset = Endomorphism-poset H Δ⁺ - module H⟨Δ⁺⟩→-poset = Reasoning H⟨Δ⁺⟩→-poset - - H⟨Δ⁺⟩→ : Displacement-on H⟨Δ⁺⟩→-poset - H⟨Δ⁺⟩→ = Endomorphism H Δ⁺ - module H⟨Δ⁺⟩→ = Displacement-on H⟨Δ⁺⟩→ + H⟨Δ⁺⟩→ : Poset (lsuc (o ⊔ r)) (o ⊔ r) + H⟨Δ⁺⟩→ = Endomorphism-poset H Δ⁺ + module H⟨Δ⁺⟩→ = Reasoning H⟨Δ⁺⟩→ SOrd : Precategory (lsuc (o ⊔ r)) (o ⊔ r) SOrd = Strict-orders o r @@ -89,7 +82,7 @@ module Mugen.Cat.HierarchyTheory.Universality.EndomorphismEmbeddingNaturality SOrd↑ = Strict-orders (lsuc (o ⊔ r)) (lsuc (o ⊔ r)) SOrdᴹᴰ : Precategory (lsuc (lsuc (o ⊔ r))) (lsuc (lsuc (o ⊔ r))) - SOrdᴹᴰ = Eilenberg-Moore SOrd↑ (McBride H⟨Δ⁺⟩→) + SOrdᴹᴰ = Eilenberg-Moore SOrd↑ (McBride 𝒟) module SOrdᴹᴰ = Cat SOrdᴹᴰ Uᴴ : Functor SOrdᴴ SOrd @@ -105,13 +98,13 @@ module Mugen.Cat.HierarchyTheory.Universality.EndomorphismEmbeddingNaturality Fᴴ₁ = Fᴴ .Functor.F₁ Uᴹᴰ : Functor SOrdᴹᴰ SOrd↑ - Uᴹᴰ = Forget SOrd↑ (McBride H⟨Δ⁺⟩→) + Uᴹᴰ = Forget SOrd↑ (McBride 𝒟) -------------------------------------------------------------------------------- -- Constructing the natural transformation ν -- Section 3.4, Lemma 3.8 - ν : (pt : ∣ Ψ ∣) + ν : ∣ Ψ ∣ → liftᶠ-strict-orders F∘ Uᴴ F∘ Endos-include => Uᴹᴰ F∘ Endos-include F∘ T ν pt = nt @@ -140,7 +133,7 @@ module Mugen.Cat.HierarchyTheory.Universality.EndomorphismEmbeddingNaturality H.μ Δ⁺ # (H.M₁ (H.μ Δ⁺ ∘ H.M₁ (ℓ̅ ℓ)) # α) ∎ abstract - ν′-mono : ∀ {ℓ′ ℓ : ⌞ H.M₀ Δ ⌟} → ℓ′ H⟨Δ⟩.≤ ℓ → ν′ ℓ′ H⟨Δ⁺⟩→-poset.≤ ν′ ℓ + ν′-mono : ∀ {ℓ′ ℓ : ⌞ H.M₀ Δ ⌟} → ℓ′ H⟨Δ⟩.≤ ℓ → ν′ ℓ′ H⟨Δ⁺⟩→.≤ ν′ ℓ ν′-mono {ℓ′} {ℓ} ℓ′≤ℓ α = begin-≤ H.μ Δ⁺ # (H.M₁ (ℓ̅ ℓ′) # (H.η Δ⁺ # α)) ≐⟨ μ-η H (ℓ̅ ℓ′) #ₚ α ⟩ ℓ̅ ℓ′ # α ≤⟨ ℓ̅-pres-≤ ℓ′≤ℓ α ⟩ diff --git a/src/Mugen/Cat/HierarchyTheory/Universality/SubcategoryEmbedding.agda b/src/Mugen/Cat/HierarchyTheory/Universality/SubcategoryEmbedding.agda index 62c3157..d7d36d3 100644 --- a/src/Mugen/Cat/HierarchyTheory/Universality/SubcategoryEmbedding.agda +++ b/src/Mugen/Cat/HierarchyTheory/Universality/SubcategoryEmbedding.agda @@ -84,10 +84,6 @@ module Mugen.Cat.HierarchyTheory.Universality.SubcategoryEmbedding {o o' r} FᴴΔ₋ : I → Algebra SOrd H FᴴΔ₋ i = Fᴴ₀ (Δ₋ i) - -- '↑' for lifting - SOrd↑ : Precategory (lsuc (lsuc o)) (lsuc o) - SOrd↑ = Strict-orders (lsuc o) (lsuc o) - pattern ι n i α = (n , i , α) ι-inj : ∀ {n : Nat} {i : I} {x y : ⌞ Δ₋ i ⌟} → _≡_ {A = ⌞ Δ ⌟} (ι n i x) (ι n i y) → x ≡ y diff --git a/src/Mugen/Everything.agda b/src/Mugen/Everything.agda index eaa1006..c97393f 100644 --- a/src/Mugen/Everything.agda +++ b/src/Mugen/Everything.agda @@ -23,6 +23,7 @@ import Mugen.Algebra.OrderedMonoid import Mugen.Cat.Endomorphisms import Mugen.Cat.HierarchyTheory import Mugen.Cat.HierarchyTheory.McBride +import Mugen.Cat.HierarchyTheory.Universality import Mugen.Cat.HierarchyTheory.Universality.EndomorphismEmbedding import Mugen.Cat.HierarchyTheory.Universality.EndomorphismEmbeddingNaturality import Mugen.Cat.HierarchyTheory.Universality.SubcategoryEmbedding