From ce83fdd640ba3b7d1c0d1f84a48081da50213296 Mon Sep 17 00:00:00 2001 From: favonia Date: Sun, 26 May 2024 14:11:39 -0500 Subject: [PATCH] feat: lemma 3.9 (#50) --- src/Mugen/Cat/Endomorphisms.agda | 19 +- .../Universality/EndomorphismEmbedding.agda | 4 +- .../Universality/HeterogeneousEmbedding.agda | 321 ++++++++++++++++++ src/Mugen/Cat/Indexed.agda | 23 ++ src/Mugen/Everything.agda | 2 + 5 files changed, 353 insertions(+), 16 deletions(-) create mode 100644 src/Mugen/Cat/HierarchyTheory/Universality/HeterogeneousEmbedding.agda create mode 100644 src/Mugen/Cat/Indexed.agda diff --git a/src/Mugen/Cat/Endomorphisms.agda b/src/Mugen/Cat/Endomorphisms.agda index bec6d12..c0a01a3 100644 --- a/src/Mugen/Cat/Endomorphisms.agda +++ b/src/Mugen/Cat/Endomorphisms.agda @@ -1,10 +1,6 @@ open import Cat.Prelude -module Mugen.Cat.Endomorphisms {o ℓ} (𝒞 : Precategory o ℓ) where - -import Cat.Reasoning as Cat - -open Cat 𝒞 +module Mugen.Cat.Endomorphisms {o ℓ} (𝒞 : Precategory o ℓ) (X : 𝒞 .Precategory.Ob) where -------------------------------------------------------------------------------- -- The category of endomorphisms on an object. @@ -12,12 +8,7 @@ open Cat 𝒞 -- /Technically/ this is a monoid, but it's easier to work with -- in this form w/o having to introduce a delooping. -Endos : Ob → Precategory lzero ℓ -Endos X .Precategory.Ob = ⊤ -Endos X .Precategory.Hom _ _ = Hom X X -Endos X .Precategory.Hom-set _ _ = Hom-set X X -Endos X .Precategory.id = id -Endos X .Precategory._∘_ = _∘_ -Endos X .Precategory.idr = idr -Endos X .Precategory.idl = idl -Endos X .Precategory.assoc = assoc +open import Mugen.Cat.Indexed + +Endos = Indexed 𝒞 {I = ⊤} λ _ → X +Endos-include = Indexed-include 𝒞 {I = ⊤} λ _ → X diff --git a/src/Mugen/Cat/HierarchyTheory/Universality/EndomorphismEmbedding.agda b/src/Mugen/Cat/HierarchyTheory/Universality/EndomorphismEmbedding.agda index a0ba439..a972e6d 100644 --- a/src/Mugen/Cat/HierarchyTheory/Universality/EndomorphismEmbedding.agda +++ b/src/Mugen/Cat/HierarchyTheory/Universality/EndomorphismEmbedding.agda @@ -204,9 +204,9 @@ module Mugen.Cat.HierarchyTheory.Universality.EndomorphismEmbedding abstract T-faithful : ∣ Ψ ∣ → preserves-monos H → is-faithful T - T-faithful pt H-preserves-monos {x} {y} {σ} {δ} p = + T-faithful pt H-preserves-monos {x} {y} {σ} {δ} eq = free-algebra-hom-path H $ H-preserves-monos ι₁-hom ι₁-monic _ _ $ ext λ α → σ̅ σ # ι₁ α ≡˘⟨ μ-η H (σ̅ σ) #ₚ ι₁ α ⟩ - H.μ _ # (H.M₁ (σ̅ σ) # (H.η _ # ι₁ α)) ≡⟨ ap snd (p #ₚ (pt , SOrdᴴ.id)) #ₚ _ ⟩ + H.μ _ # (H.M₁ (σ̅ σ) # (H.η _ # ι₁ α)) ≡⟨ ap snd (eq #ₚ (pt , SOrdᴴ.id)) #ₚ (H.η _ # ι₁ α) ⟩ H.μ _ # (H.M₁ (σ̅ δ) # (H.η _ # ι₁ α)) ≡⟨ μ-η H (σ̅ δ) #ₚ ι₁ α ⟩ σ̅ δ # ι₁ α ∎ diff --git a/src/Mugen/Cat/HierarchyTheory/Universality/HeterogeneousEmbedding.agda b/src/Mugen/Cat/HierarchyTheory/Universality/HeterogeneousEmbedding.agda new file mode 100644 index 0000000..0d842f7 --- /dev/null +++ b/src/Mugen/Cat/HierarchyTheory/Universality/HeterogeneousEmbedding.agda @@ -0,0 +1,321 @@ +-- vim: nowrap +open import Data.Nat +open import Order.Instances.Discrete +open import Order.Instances.Disjoint + +open import Cat.Prelude +open import Cat.Functor.Base +open import Cat.Functor.Properties +open import Cat.Diagram.Monad + +import Cat.Reasoning as Cat + +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.Copower +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, Lemma 3.9 +-- +-- Naturality is in a different file + +module Mugen.Cat.HierarchyTheory.Universality.HeterogeneousEmbedding + {o} (H : Hierarchy-theory o o) {I : Type o} + ⦃ Discrete-I : Discrete I ⦄ + (Δ₋ : ⌞ I ⌟ → Poset o o) where + + -------------------------------------------------------------------------------- + -- Notation + -- + -- We begin by defining some useful notation. + + private + open Strictly-monotone + open Algebra-hom + open Cat (Strict-orders o o) + module Δ₋ i = Poset (Δ₋ i) + module H = Monad H + + ⌞Δ₋⌟ : I → Type o + ⌞Δ₋⌟ i = ⌞ Δ₋ i ⌟ + + abstract instance  + H-Level-I : H-Level I 2 + H-Level-I = hlevel-instance $ Discrete→is-set Discrete-I + + Δ' : Poset o o + Δ' = Disjoint (el! I) Δ₋ + module Δ' = Poset Δ' + + Δ : Poset o o + Δ = Copower (el! Nat) Δ' + module Δ = Poset Δ + + H⟨Δ⟩ : Poset o o + H⟨Δ⟩ = H.M₀ Δ + module H⟨Δ⟩ = Reasoning H⟨Δ⟩ + + SOrd : Precategory (lsuc o) o + SOrd = Strict-orders o o + module SOrd = Cat SOrd + + SOrdᴴ : Precategory (lsuc o) (lsuc o) + SOrdᴴ = Eilenberg-Moore SOrd H + module SOrdᴴ = Cat SOrdᴴ + + Uᴴ : Functor SOrdᴴ SOrd + Uᴴ = Forget SOrd H + + Fᴴ : Functor SOrd SOrdᴴ + Fᴴ = Free SOrd H + + Fᴴ₀ : Poset o o → Algebra SOrd H + Fᴴ₀ = Fᴴ .Functor.F₀ + + Fᴴ₁ : {X Y : Poset o o} → Hom X Y → SOrdᴴ.Hom (Fᴴ₀ X) (Fᴴ₀ Y) + Fᴴ₁ = Fᴴ .Functor.F₁ + + 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 + ι-inj p = is-set→cast-pathp ⌞Δ₋⌟ (hlevel 2) λ j → p j .snd .snd + + ι-hom : ∀ (n : Nat) (i : I) → Hom (Δ₋ i) Δ + ι-hom n i .hom = ι n i + ι-hom n i .pres-≤[]-equal α≤β = (reflᵢ , (reflᵢ , α≤β)) , ι-inj + + ι-monic : ∀ {n : Nat} {i : I} → SOrd.is-monic (ι-hom n i) + ι-monic g h eq = ext λ α → ι-inj (eq #ₚ α) + + -------------------------------------------------------------------------------- + -- Construction of the functor T + -- Section 3.4, Lemma 3.9 + + σ̅ : {i j : I} → SOrdᴴ.Hom (FᴴΔ₋ i) (FᴴΔ₋ j) → Hom Δ H⟨Δ⟩ + σ̅ {i} {j} σ .hom (ι n k α) with k ≡ᵢ? i | n | k ≡ᵢ? j + ... | yes k=ᵢi | 0 | _ = H.M₁ (ι-hom 0 j) # (σ # (H.η (Δ₋ i) # substᵢ ⌞Δ₋⌟ k=ᵢi α)) -- case k0j + ... | yes _ | suc n | yes _ = H.η Δ # ι (suc n) k α -- case k1k + ... | yes _ | suc n | no _ = H.η Δ # ι n k α -- case k1j + ... | no _ | n | yes _ = H.η Δ # ι (suc n) k α -- case ik + ... | no _ | n | no _ = H.η Δ # ι n k α -- case ij + σ̅ {i} {j} σ .pres-≤[]-equal {ι n k α} {ι n k β} (reflᵢ , reflᵢ , α≤β) with k ≡ᵢ? i | n | k ≡ᵢ? j + ... | yes reflᵢ | 0 | _ = H⟨Δ⟩.≤[]-map (ap (ι 0 i)) $ (H.M₁ (ι-hom 0 j) ∘ σ .morphism ∘ H.η (Δ₋ i)) .pres-≤[]-equal α≤β + ... | yes reflᵢ | suc n | yes _ = H.η Δ .pres-≤[]-equal (reflᵢ , reflᵢ , α≤β) + ... | yes reflᵢ | suc n | no _ = H⟨Δ⟩.≤[]-map (ap (ι (suc n) k)) $ (H.η Δ ∘ ι-hom n k) .pres-≤[]-equal α≤β + ... | no _ | n | yes _ = H⟨Δ⟩.≤[]-map (ap (ι n k)) $ (H.η Δ ∘ ι-hom (suc n) k) .pres-≤[]-equal α≤β + ... | no _ | n | no _ = H.η Δ .pres-≤[]-equal (reflᵢ , reflᵢ , α≤β) + + -- all raw β rules + module _ where + abstract + σ̅-ι-k0j-ext : ∀ {i j k : I} (σ : SOrdᴴ.Hom (FᴴΔ₋ i) (FᴴΔ₋ j)) + → (p : k ≡ᵢ i) + → (α : ⌞ Δ₋ k ⌟) + → σ̅ σ # ι 0 k α ≡ H.M₁ (ι-hom 0 j) # (σ # (H.η (Δ₋ i) # substᵢ ⌞Δ₋⌟ p α)) + σ̅-ι-k0j-ext {i = i} {j} {k} σ p α with k ≡ᵢ? i + ... | no k≠ᵢi = absurd (k≠ᵢi p) + ... | yes k=ᵢi = + H.M₁ (ι-hom 0 j) # (σ # (H.η (Δ₋ i) # substᵢ ⌞Δ₋⌟ k=ᵢi α)) + ≡⟨ ap# (H.M₁ (ι-hom 0 j) ∘ σ .morphism ∘ H.η (Δ₋ i)) + (λ l → substᵢ ⌞Δ₋⌟ (hlevel 1 k=ᵢi p l) α) ⟩ + H.M₁ (ι-hom 0 j) # (σ # (H.η (Δ₋ i) # substᵢ ⌞Δ₋⌟ p α)) + ∎ + + σ̅-ι-k1k-ext : ∀ (n : Nat) {i j k : I} (σ : SOrdᴴ.Hom (Fᴴ₀ (Δ₋ i)) (Fᴴ₀ (Δ₋ j))) + → k ≡ᵢ i + → k ≡ᵢ j + → (α : ⌞ Δ₋ k ⌟) + → σ̅ σ # ι (suc n) k α ≡ H.η Δ # ι (suc n) k α + σ̅-ι-k1k-ext n {i = i} {j} {k} σ k=ᵢi k=ᵢj α with k ≡ᵢ? i | k ≡ᵢ? j + ... | no k≠ᵢi | _ = absurd (k≠ᵢi k=ᵢi) + ... | yes _ | no k≠ᵢj = absurd (k≠ᵢj k=ᵢj) + ... | yes _ | yes _ = refl + + σ̅-ι-k1j-ext : ∀ (n : Nat) {i j k : I} (σ : SOrdᴴ.Hom (Fᴴ₀ (Δ₋ i)) (Fᴴ₀ (Δ₋ j))) + → k ≡ᵢ i + → ¬ (k ≡ᵢ j) + → (α : ⌞ Δ₋ k ⌟) + → σ̅ σ # ι (suc n) k α ≡ H.η Δ # ι n k α + σ̅-ι-k1j-ext n {i = i} {j} {k} σ k=ᵢi k≠ᵢj α with k ≡ᵢ? i | k ≡ᵢ? j + ... | no k≠ᵢi | _ = absurd (k≠ᵢi k=ᵢi) + ... | yes _ | yes k=ᵢj = absurd (k≠ᵢj k=ᵢj) + ... | yes _ | no _ = refl + + σ̅-ι-ik-ext : ∀ (n : Nat) {i j k : I} (σ : SOrdᴴ.Hom (Fᴴ₀ (Δ₋ i)) (Fᴴ₀ (Δ₋ j))) + → ¬ (k ≡ᵢ i) + → k ≡ᵢ j + → (α : ⌞ Δ₋ k ⌟) + → σ̅ σ # ι n k α ≡ H.η Δ # ι (suc n) k α + σ̅-ι-ik-ext n {i = i} {j} {k} σ k≠ᵢi k=ᵢj α with k ≡ᵢ? i | k ≡ᵢ? j + ... | yes k=ᵢi | _ = absurd (k≠ᵢi k=ᵢi) + ... | no _ | no k≠ᵢj = absurd (k≠ᵢj k=ᵢj) + ... | no _ | yes _ = refl + + σ̅-ι-ij-ext : ∀ (n : Nat) {i j k : I} (σ : SOrdᴴ.Hom (Fᴴ₀ (Δ₋ i)) (Fᴴ₀ (Δ₋ j))) + → ¬ (k ≡ᵢ i) + → ¬ (k ≡ᵢ j) + → (α : ⌞ Δ₋ k ⌟) + → σ̅ σ # ι n k α ≡ H.η Δ # ι n k α + σ̅-ι-ij-ext n {i = i} {j} {k} σ k≠ᵢi k≠ᵢj α with k ≡ᵢ? i | k ≡ᵢ? j + ... | yes k=ᵢi | _ = absurd (k≠ᵢi k=ᵢi) + ... | no _ | yes k=ᵢj = absurd (k≠ᵢj k=ᵢj) + ... | no _ | no _ = refl + + -- all wrapped β rules + module _ where + abstract + H-σ̅-ι-k0j : ∀ {k j : I} (σ : SOrdᴴ.Hom (FᴴΔ₋ k) (FᴴΔ₋ j)) (α : ⌞ H.M₀ (Δ₋ k) ⌟) + → H.μ Δ # (H.M₁ (σ̅ σ) # (H.M₁ (ι-hom 0 k) # α)) + ≡ H.M₁ (ι-hom 0 j) # (σ # α) + H-σ̅-ι-k0j {k = k} {j} σ α = + H.μ Δ # (H.M₁ (σ̅ σ) # (H.M₁ (ι-hom 0 k) # α)) + ≡˘⟨ ap# (H.μ Δ) $ H.M-∘ (σ̅ σ) (ι-hom 0 k) #ₚ α ⟩ + H.μ Δ # (H.M₁ (σ̅ σ ∘ ι-hom 0 k) # α) + ≡⟨ ap (λ m → H.μ Δ # (H.M₁ m # α)) $ ext $ σ̅-ι-k0j-ext σ reflᵢ ⟩ + H.μ Δ # (H.M₁ (H.M₁ (ι-hom 0 j) ∘ σ .morphism ∘ H.η (Δ₋ k)) # α) + ≡⟨ μ-M-∘-M H (ι-hom 0 j) (σ .morphism ∘ H.η (Δ₋ k)) #ₚ α ⟩ + H.M₁ (ι-hom 0 j) # (H.μ (Δ₋ j) # (H.M₁ (σ .morphism ∘ H.η (Δ₋ k)) # α)) + ≡⟨ ap# (H.M₁ (ι-hom 0 j)) $ μ-M-∘-Algebraic H σ (H.η (Δ₋ k)) #ₚ α ⟩ + H.M₁ (ι-hom 0 j) # (σ # (H.μ (Δ₋ k) # (H.M₁ (H.η (Δ₋ k)) # α))) + ≡⟨ ap# (H.M₁ (ι-hom 0 j) ∘ σ .morphism) $ H.left-ident #ₚ _ ⟩ + H.M₁ (ι-hom 0 j) # (σ # α) + ∎ + + H-σ̅-η-ι-k1k : ∀ (n : Nat) {i : I} (σ : SOrdᴴ.Hom (Fᴴ₀ (Δ₋ i)) (Fᴴ₀ (Δ₋ i))) + → (α : ⌞ Δ₋ i ⌟) + → H.μ Δ # (H.M₁ (σ̅ σ) # (H.η Δ # ι (suc n) i α)) + ≡ H.η Δ # ι (suc n) i α + H-σ̅-η-ι-k1k n {i = i} σ α = + H.μ Δ # (H.M₁ (σ̅ σ) # (H.η Δ # ι (suc n) i α)) + ≡⟨ μ-η H (σ̅ σ) #ₚ _ ⟩ + σ̅ σ # ι (suc n) i α + ≡⟨ σ̅-ι-k1k-ext n σ reflᵢ reflᵢ α ⟩ + H.η Δ # ι (suc n) i α + ∎ + + H-σ̅-η-ι-k1j : ∀ (n : Nat) {k j : I} (σ : SOrdᴴ.Hom (Fᴴ₀ (Δ₋ k)) (Fᴴ₀ (Δ₋ j))) + → ¬ (k ≡ᵢ j) + → (α : ⌞ Δ₋ k ⌟) + → H.μ Δ # (H.M₁ (σ̅ σ) # (H.η Δ # ι (suc n) k α)) + ≡ H.η Δ # ι n k α + H-σ̅-η-ι-k1j n {k = k} σ k≠j α = + H.μ Δ # (H.M₁ (σ̅ σ) # (H.η Δ # ι (suc n) k α)) + ≡⟨ μ-η H (σ̅ σ) #ₚ _ ⟩ + σ̅ σ # ι (suc n) k α + ≡⟨ σ̅-ι-k1j-ext n σ reflᵢ k≠j α ⟩ + H.η Δ # ι n k α + ∎ + + H-σ̅-η-ι-ik : ∀ (n : Nat) {i k : I} (σ : SOrdᴴ.Hom (Fᴴ₀ (Δ₋ i)) (Fᴴ₀ (Δ₋ k))) + → ¬ (k ≡ᵢ i) + → (α : ⌞ Δ₋ k ⌟) + → H.μ Δ # (H.M₁ (σ̅ σ) # (H.η Δ # ι n k α)) + ≡ H.η Δ # ι (suc n) k α + H-σ̅-η-ι-ik n {i = i} {k} σ k≠i α = + H.μ Δ # (H.M₁ (σ̅ σ) # (H.η Δ # ι n k α)) + ≡⟨ μ-η H (σ̅ σ) #ₚ _ ⟩ + σ̅ σ # ι n k α + ≡⟨ σ̅-ι-ik-ext n σ k≠i reflᵢ α ⟩ + H.η Δ # ι (suc n) k α + ∎ + + H-σ̅-η-ι-ij : ∀ (n : Nat) {i j k : I} (σ : SOrdᴴ.Hom (Fᴴ₀ (Δ₋ i)) (Fᴴ₀ (Δ₋ j))) + → ¬ (k ≡ᵢ i) + → ¬ (k ≡ᵢ j) + → (α : ⌞ Δ₋ k ⌟) + → H.μ Δ # (H.M₁ (σ̅ σ) # (H.η Δ # ι n k α)) + ≡ H.η Δ # ι n k α + H-σ̅-η-ι-ij n {i = i} {j} {k} σ k≠i k≠j α = + H.μ Δ # (H.M₁ (σ̅ σ) # (H.η Δ # ι n k α)) + ≡⟨ μ-η H (σ̅ σ) #ₚ _ ⟩ + σ̅ σ # ι n k α + ≡⟨ σ̅-ι-ij-ext n σ k≠i k≠j α ⟩ + H.η Δ # ι n k α + ∎ + + abstract + σ̅-id : ∀ {i : I} (n : Nat) (k : I) (α : ⌞ Δ₋ k ⌟) → + σ̅ {i = i} SOrdᴴ.id # ι n k α ≡ H.η Δ # ι n k α + σ̅-id {i = i} n k α with k ≡ᵢ? i | n + ... | yes reflᵢ | 0 = sym (H.unit.is-natural (Δ₋ i) Δ (ι-hom 0 i)) #ₚ α + ... | yes reflᵢ | suc n = refl + ... | no _ | n = refl + + abstract + σ̅-∘ : ∀ {i j k : I} + (σ : SOrdᴴ.Hom (FᴴΔ₋ j) (FᴴΔ₋ k)) + (δ : SOrdᴴ.Hom (FᴴΔ₋ i) (FᴴΔ₋ j)) + (n : Nat) (l : I) (α : ⌞Δ₋⌟ l) + → σ̅ (σ SOrdᴴ.∘ δ) # ι n l α + ≡ (H.μ Δ ∘ H.M₁ (σ̅ σ) ∘ σ̅ δ) # ι n l α + σ̅-∘ {i = i} {j} {k} σ δ n l α with l ≡ᵢ? i | n | l ≡ᵢ? j | l ≡ᵢ? k + ... | yes reflᵢ | 0 | _ | _ = sym $ H-σ̅-ι-k0j σ (δ # (H.η (Δ₋ i) # α)) + ... | yes reflᵢ | suc n | yes reflᵢ | yes reflᵢ = sym $ H-σ̅-η-ι-k1k n σ α + ... | yes reflᵢ | suc n | yes reflᵢ | no l≠k = sym $ H-σ̅-η-ι-k1j n σ l≠k α + ... | yes reflᵢ | suc n | no l≠j | yes reflᵢ = sym $ H-σ̅-η-ι-ik n σ l≠j α + ... | yes reflᵢ | suc n | no l≠j | no l≠k = sym $ H-σ̅-η-ι-ij n σ l≠j l≠k α + ... | no l≠i | n | yes reflᵢ | yes reflᵢ = sym $ H-σ̅-η-ι-k1k n σ α + ... | no l≠i | n | yes reflᵢ | no l≠k = sym $ H-σ̅-η-ι-k1j n σ l≠k α + ... | no l≠i | n | no l≠j | yes reflᵢ = sym $ H-σ̅-η-ι-ik n σ l≠j α + ... | no l≠i | n | no l≠j | no l≠k = sym $ H-σ̅-η-ι-ij n σ l≠j l≠k α + + T : Functor (Indexed SOrdᴴ FᴴΔ₋) (Endos SOrdᴴ (Fᴴ₀ Δ)) + T .Functor.F₀ i = tt + T .Functor.F₁ σ .morphism = H.μ Δ ∘ H.M₁ (σ̅ σ) + T .Functor.F₁ σ .commutes = ext λ α → + H.μ Δ # (H.M₁ (σ̅ σ) # (H.μ Δ # α)) ≡˘⟨ ap# (H.μ _) $ H.mult.is-natural _ _ (σ̅ σ) #ₚ α ⟩ + H.μ Δ # (H.μ (H.M₀ Δ) # (H.M₁ (H.M₁ (σ̅ σ)) # α)) ≡˘⟨ μ-M-∘-μ H (H.M₁ (σ̅ σ)) #ₚ α ⟩ + H.μ Δ # (H.M₁ (H.μ Δ ∘ H.M₁ (σ̅ σ)) # α) ∎ + T .Functor.F-id = ext λ α → + H.μ _ # (H.M₁ (σ̅ SOrdᴴ.id) # α) ≡⟨ ap (λ m → H.μ _ # (H.M₁ m # α)) $ ext σ̅-id ⟩ + H.μ _ # (H.M₁ (H.η _) # α) ≡⟨ H.left-ident #ₚ _ ⟩ + α ∎ + T .Functor.F-∘ σ δ = ext λ α → + H.μ Δ # (H.M₁ (σ̅ (σ SOrdᴴ.∘ δ)) # α) ≡⟨ ap# (H.μ Δ) $ ap (H.M₁) (ext $ σ̅-∘ σ δ) #ₚ α ⟩ + H.μ Δ # (H.M₁ (H.μ Δ ∘ H.M₁ (σ̅ σ) ∘ σ̅ δ) # α) ≡⟨ μ-M-∘-μ H (H.M₁ (σ̅ σ) ∘ σ̅ δ) #ₚ α ⟩ + H.μ Δ # (H.μ (H.M₀ Δ) # (H.M₁ (H.M₁ (σ̅ σ) ∘ σ̅ δ) # α)) ≡⟨ ap# (H.μ Δ) $ μ-M-∘-M H (σ̅ σ) (σ̅ δ) #ₚ α ⟩ + H.μ Δ # (H.M₁ (σ̅ σ) # (H.μ Δ # (H.M₁ (σ̅ δ) # α))) ∎ + + -------------------------------------------------------------------------------- + -- Constructing the natural transformation ν + -- Section 3.4, Lemma 3.8 + + ν : Uᴴ F∘ Indexed-include SOrdᴴ FᴴΔ₋ => Uᴴ F∘ Endos-include SOrdᴴ (Fᴴ₀ Δ) F∘ T + ν ._=>_.η i = H.M₁ (ι-hom 0 i) + ν ._=>_.is-natural i j σ = sym $ ext $ H-σ̅-ι-k0j σ + + -------------------------------------------------------------------------------- + -- Faithfulness of T + -- Section 3.4, Lemma 3.9 + + abstract + T-faithful : preserves-monos H → is-faithful T + T-faithful H-preserves-monos {i} {j} {σ} {δ} eq = + Algebra-hom-path _ $ H-preserves-monos (ι-hom 0 j) ι-monic _ _ $ ext λ α → + H.M₁ (ι-hom 0 j) # (σ # α) ≡˘⟨ H-σ̅-ι-k0j σ α ⟩ + H.μ Δ # (H.M₁ (σ̅ σ) # (H.M₁ (ι-hom 0 i) # α)) ≡⟨ eq #ₚ (H.M₁ (ι-hom 0 i) # α) ⟩ + H.μ Δ # (H.M₁ (σ̅ δ) # (H.M₁ (ι-hom 0 i) # α)) ≡⟨ H-σ̅-ι-k0j δ α ⟩ + H.M₁ (ι-hom 0 j) # (δ # α) ∎ diff --git a/src/Mugen/Cat/Indexed.agda b/src/Mugen/Cat/Indexed.agda new file mode 100644 index 0000000..787e778 --- /dev/null +++ b/src/Mugen/Cat/Indexed.agda @@ -0,0 +1,23 @@ +open import Cat.Prelude + +module Mugen.Cat.Indexed {o o' ℓ} (𝒞 : Precategory o ℓ) {I : Type o'} (F : I → 𝒞 .Precategory.Ob) where + +import Cat.Reasoning as Cat + +open Cat 𝒞 + +Indexed : Precategory o' ℓ +Indexed .Precategory.Ob = I +Indexed .Precategory.Hom i j = Hom (F i) (F j) +Indexed .Precategory.Hom-set _ _ = Hom-set _ _ +Indexed .Precategory.id = id +Indexed .Precategory._∘_ = _∘_ +Indexed .Precategory.idr = idr +Indexed .Precategory.idl = idl +Indexed .Precategory.assoc = assoc + +Indexed-include : Functor Indexed 𝒞 +Indexed-include .Functor.F₀ = F +Indexed-include .Functor.F₁ σ = σ +Indexed-include .Functor.F-id = refl +Indexed-include .Functor.F-∘ _ _ = refl diff --git a/src/Mugen/Everything.agda b/src/Mugen/Everything.agda index e8530c9..c4d12e0 100644 --- a/src/Mugen/Everything.agda +++ b/src/Mugen/Everything.agda @@ -25,6 +25,8 @@ import Mugen.Cat.HierarchyTheory import Mugen.Cat.HierarchyTheory.McBride import Mugen.Cat.HierarchyTheory.Universality.EndomorphismEmbedding import Mugen.Cat.HierarchyTheory.Universality.EndomorphismEmbeddingNaturality +import Mugen.Cat.HierarchyTheory.Universality.HeterogeneousEmbedding +import Mugen.Cat.Indexed import Mugen.Cat.Monad import Mugen.Cat.StrictOrders import Mugen.Data.List