feat: theorem 3.10 (#53)

RedPRL · May 29, 2024 · ce35155 · ce35155
1 parent 000df03
commit ce35155
Show file tree

Hide file tree

Showing 6 changed files with 162 additions and 32 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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