Skip to content

Commit

Permalink
WIP: core lemma of functorness done!
Browse files Browse the repository at this point in the history
  • Loading branch information
@favonia
favonia committed May 25, 2024
1 parent 4c348f4 commit 9a2ab8d
Show file tree
Hide file tree
Showing 3 changed files with 252 additions and 188 deletions.
102 changes: 48 additions & 54 deletions src/Mugen/Cat/HierarchyTheory/Universality/EndomorphismEmbedding.agda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -84,11 +84,14 @@ module Mugen.Cat.HierarchyTheory.Universality.EndomorphismEmbedding
SOrdᴹᴰ = Eilenberg-Moore SOrd↑ (McBride H⟨Δ⁺⟩→)
module SOrdᴹᴰ = Cat SOrdᴹᴰ

Fᴴ⟨_⟩ : Poset o r → Algebra SOrd H
Fᴴ⟨_⟩ = Functor.F₀ (Free SOrd H)
Fᴴ₀ : Poset o r → Algebra SOrd H
Fᴴ₀ = Functor.F₀ (Free SOrd H)

Fᴴ₁ : {X Y : Poset o r} → Hom X Y → Algebra-hom SOrd H (Fᴴ₀ X) (Fᴴ₀ Y)
Fᴴ₁ = Functor.F₁ (Free SOrd H)

Endoᴴ⟨Δ⟩ : Type (o ⊔ r)
Endoᴴ⟨Δ⟩ = Hom (Fᴴ⟨ Δ ⟩ .fst) (Fᴴ⟨ Δ ⟩ .fst)
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⟨Δ⁺⟩→))
Expand Down Expand Up @@ -126,69 +129,62 @@ module Mugen.Cat.HierarchyTheory.Universality.EndomorphismEmbedding
-- Construction of the functor T
-- Section 3.4, Lemma 3.8

σ̅ : Algebra-hom SOrd H Fᴴ⟨ Δ ⟩ Fᴴ⟨ Δ ⟩ → Hom Δ⁺ H⟨Δ⁺⟩
σ̅ σ .hom (ι₀ ⋆) = H.unit.η Δ⁺ # ι₀ ⋆
σ̅ σ .hom (ι₁ α) = H.M₁ ι₁-hom # (σ # (H.unit.η Δ # α))
σ̅ σ .hom (ι₂ α) = H.unit.η Δ⁺ # ι₂ α
σ̅ : Algebra-hom SOrd H (Fᴴ₀ Δ) (Fᴴ₀ Δ) → Hom Δ⁺ H⟨Δ⁺⟩
σ̅ σ .hom (ι₀ ⋆) = H.η Δ⁺ # ι₀ ⋆
σ̅ σ .hom (ι₁ α) = H.M₁ ι₁-hom # (σ # (H.η Δ # α))
σ̅ σ .hom (ι₂ α) = H.η Δ⁺ # ι₂ α
σ̅ σ .pres-≤[]-equal {ι₀ ⋆} {ι₀ ⋆} _ = H⟨Δ⁺⟩.≤-refl , λ _ → refl
σ̅ σ .pres-≤[]-equal {ι₁ α} {ι₁ β} (lift (lift α≤β)) = H⟨Δ⁺⟩.≤[]-map (ap ι₁) $ (H.M₁ ι₁-hom ∘ σ .morphism ∘ H.unit.η Δ) .pres-≤[]-equal α≤β
σ̅ σ .pres-≤[]-equal {ι₂ α} {ι₂ β} α≤β = H.unit.η Δ⁺ .pres-≤[]-equal α≤β
σ̅ σ .pres-≤[]-equal {ι₁ α} {ι₁ β} (lift (lift α≤β)) = H⟨Δ⁺⟩.≤[]-map (ap ι₁) $ (H.M₁ ι₁-hom ∘ σ .morphism ∘ H.η Δ) .pres-≤[]-equal α≤β
σ̅ σ .pres-≤[]-equal {ι₂ α} {ι₂ β} α≤β = H.η Δ⁺ .pres-≤[]-equal α≤β

abstract
σ̅-id : σ̅ SOrdᴴ.id ≡ H.unit.η Δ⁺
σ̅-id : σ̅ SOrdᴴ.id ≡ H.η Δ⁺
σ̅-id = ext λ where
(ι₀ α) → refl
(ι₁ α) → sym (H.unit.is-natural Δ Δ⁺ ι₁-hom) #ₚ α
(ι₂ α) → refl

abstract
σ̅-ι
: ∀ (σ : Algebra-hom SOrd H Fᴴ⟨ Δ ⟩ Fᴴ⟨ Δ ⟩)
: ∀ (σ : Algebra-hom SOrd H (Fᴴ₀ Δ) (Fᴴ₀ Δ))
→ (α : ⌞ H.M₀ Δ ⌟)
→ H.M₁ (H.M₁ ι₁-hom) # (H.M₁ (σ .morphism) # (H.M₁ (H.unit.η Δ) # α))
→ H.M₁ (H.M₁ ι₁-hom ∘ σ .morphism ∘ H.η Δ) # α
≡ H.M₁ (σ̅ σ) # (H.M₁ ι₁-hom # α)
σ̅-ι σ α =
(H.M₁ (H.M₁ ι₁-hom) ∘ H.M₁ (σ .morphism) ∘ H.M₁ (H.unit.η Δ)) # α ≡˘⟨ ap (H.M₁ (H.M₁ ι₁-hom) ∘_) (H.M-∘ _ _) #ₚ α ⟩
(H.M₁ (H.M₁ ι₁-hom) ∘ H.M₁ (σ .morphism ∘ H.unit.η Δ)) # α ≡˘⟨ H.M-∘ _ _ #ₚ α ⟩
H.M₁ (H.M₁ ι₁-hom ∘ σ .morphism ∘ H.unit.η Δ) # α ≡⟨ ap H.M₁ lemma #ₚ α ⟩
H.M₁ (σ̅ σ ∘ ι₁-hom) # α ≡⟨ H.M-∘ _ _ #ₚ α ⟩
H.M₁ (σ̅ σ) # (H.M₁ ι₁-hom # α) ∎
where
lemma : H.M₁ ι₁-hom ∘ σ .morphism ∘ H.unit.η Δ ≡ σ̅ σ ∘ ι₁-hom
lemma = ext λ _ → refl
H.M₁ (H.M₁ ι₁-hom ∘ σ .morphism ∘ H.η Δ) # α ≡⟨ ap (λ m → H.M₁ m # α) $ ext (λ _ → refl) ⟩
H.M₁ (σ̅ σ ∘ ι₁-hom) # α ≡⟨ H.M-∘ _ _ #ₚ α ⟩
H.M₁ (σ̅ σ) # (H.M₁ ι₁-hom # α) ∎

abstract
σ̅-∘ : ∀ (σ δ : Algebra-hom SOrd H Fᴴ⟨ Δ ⟩ Fᴴ⟨ Δ ⟩) → σ̅ (σ SOrdᴴ.∘ δ) ≡ H.mult.η Δ⁺ ∘ H.M₁ (σ̅ σ) ∘ σ̅ δ
σ̅-∘ : ∀ (σ δ : Algebra-hom SOrd H (Fᴴ₀ Δ) (Fᴴ₀ Δ)) → σ̅ (σ SOrdᴴ.∘ δ) ≡ H.μ Δ⁺ ∘ H.M₁ (σ̅ σ) ∘ σ̅ δ
σ̅-∘ σ δ = ext λ where
(ι₀ α) →
H.unit.η Δ⁺ # ι₀ α ≡˘⟨ H.right-ident #ₚ (H.unit.η Δ⁺ # ι₀ α) ⟩
H.mult.η Δ⁺ # (H.unit.η (H.M₀ Δ⁺) # (H.unit.η Δ⁺ # ι₀ α)) ≡⟨ ap# (H.mult.η _) (H.unit.is-natural _ _ (σ̅ σ) #ₚ ι₀ α) ⟩
H.mult.η Δ⁺ # (H.M₁ (σ̅ σ) # (H.unit.η Δ⁺ # ι₀ α)) ∎
H.η Δ⁺ # ι₀ α ≡˘⟨ μ-η H (σ̅ σ) #ₚ ι₀ α ⟩
H.μ Δ⁺ # (H.M₁ (σ̅ σ) # (H.η Δ⁺ # ι₀ α)) ∎
(ι₁ α) →
H.M₁ ι₁-hom # (σ # (δ # (H.unit.η Δ # α))) ≡˘⟨ ap# (H.M₁ ι₁-hom ∘ σ .morphism) $ H.left-ident #ₚ _ ⟩
H.M₁ ι₁-hom # (σ # (H.mult.η Δ # (H.M₁ (H.unit.η Δ) # (δ # (H.unit.η Δ # α))))) ≡⟨ ap# (H.M₁ ι₁-hom) (σ .commutes #ₚ _) ⟩
H.M₁ ι₁-hom # (H.mult.η _ # (H.M₁ (σ .morphism) # (H.M₁ (H.unit.η Δ) # (δ # (H.unit.η Δ # α))))) ≡˘⟨ H.mult.is-natural _ _ ι₁-hom #ₚ _ ⟩
H.mult.η _ # (H.M₁ (H.M₁ ι₁-hom) # (H.M₁ (σ .morphism) # (H.M₁ (H.unit.η Δ) # (δ # (H.unit.η Δ # α))))) ≡⟨ ap# (H.mult.η _) (σ̅-ι σ (δ # (H.unit.η _ # α))) ⟩
H.mult.η _ # (H.M₁ (σ̅ σ) # (H.M₁ ι₁-hom # (δ # (H.unit.η Δ # α))) ) ∎
H.M₁ ι₁-hom # (σ # (δ # (H.η Δ # α))) ≡˘⟨ ap# (H.M₁ ι₁-hom ∘ σ .morphism) $ H.left-ident #ₚ _ ⟩
H.M₁ ι₁-hom # (σ # (H.μ Δ # (H.M₁ (H.η Δ) # (δ # (H.η Δ # α))))) ≡˘⟨ ap# (H.M₁ ι₁-hom) $ μ-Algebraic H σ (H.η Δ) #ₚ _ ⟩
H.M₁ ι₁-hom # (H.μ _ # (H.M₁ (σ .morphism ∘ H.η Δ) # (δ # (H.η Δ # α)))) ≡˘⟨ μ-Algebraic H (Fᴴ₁ ι₁-hom) (σ .morphism ∘ H.η Δ) #ₚ _ ⟩
H.μ _ # (H.M₁ (H.M₁ ι₁-hom ∘ σ .morphism ∘ H.η Δ) # (δ # (H.η Δ # α))) ≡⟨ ap# (H.μ _) (σ̅-ι σ (δ # (H.η _ # α))) ⟩
H.μ _ # (H.M₁ (σ̅ σ) # (H.M₁ ι₁-hom # (δ # (H.η Δ # α)))) ∎
(ι₂ α) →
H.unit.η Δ⁺ # ι₂ α ≡˘⟨ H.right-ident #ₚ _ ⟩
H.mult.η Δ⁺ # (H.unit.η (H.M₀ Δ⁺) # (H.unit.η Δ⁺ # ι₂ α)) ≡⟨ ap# (H.mult.η _) (H.unit.is-natural _ _ (σ̅ σ) #ₚ (ι₂ α)) ⟩
H.mult.η Δ⁺ # (H.M₁ (σ̅ σ) # (H.unit.η Δ⁺ # ι₂ α)) ∎
H.η Δ⁺ # ι₂ α ≡˘⟨ μ-η H (σ̅ σ) #ₚ ι₂ α ⟩
H.μ Δ⁺ # (H.M₁ (σ̅ σ) # (H.η Δ⁺ # ι₂ α)) ∎


T′ : (σ : Algebra-hom SOrd H Fᴴ⟨ Δ ⟩ Fᴴ⟨ Δ ⟩) → Algebra-hom SOrd H Fᴴ⟨ Δ⁺ ⟩ Fᴴ⟨ Δ⁺ ⟩
T′ σ .morphism = H.mult.η Δ⁺ ∘ H.M₁ (σ̅ σ)
T′ : (σ : Algebra-hom SOrd H (Fᴴ₀ Δ) (Fᴴ₀ Δ)) → Algebra-hom SOrd H (Fᴴ₀ Δ⁺) (Fᴴ₀ Δ⁺)
T′ σ .morphism = H.μ Δ⁺ ∘ H.M₁ (σ̅ σ)
T′ σ .commutes = ext λ α →
H.mult.η Δ⁺ # (H.M₁ (σ̅ σ) # (H.mult.η Δ⁺ # α)) ≡˘⟨ ap# (H.mult.η _) $ H.mult.is-natural _ _ (σ̅ σ) #ₚ α ⟩
H.mult.η Δ⁺ # (H.mult.η (H.M₀ Δ⁺) # (H.M₁ (H.M₁ (σ̅ σ)) # α)) ≡˘⟨ H.mult-assoc #ₚ ((H.M₁ (H.M₁ (σ̅ σ))) # α) ⟩
H.mult.η Δ⁺ # (H.M₁ (H.mult.η Δ⁺) # (H.M₁ (H.M₁ (σ̅ σ)) # α)) ≡˘⟨ ap# (H.mult.η _) (H.M-∘ (H.mult.η _) (H.M₁ (σ̅ σ)) #ₚ α) ⟩
H.mult.η Δ⁺ # (H.M₁ (H.mult.η Δ⁺ ∘ H.M₁ (σ̅ σ)) # α) ∎
H.μ Δ⁺ # (H.M₁ (σ̅ σ) # (H.μ Δ⁺ # α)) ≡˘⟨ ap# (H.μ _) $ H.mult.is-natural _ _ (σ̅ σ) #ₚ α ⟩
H.μ Δ⁺ # (H.μ (H.M₀ Δ⁺) # (H.M₁ (H.M₁ (σ̅ σ)) # α)) ≡˘⟨ H.mult-assoc #ₚ ((H.M₁ (H.M₁ (σ̅ σ))) # α) ⟩
H.μ Δ⁺ # (H.M₁ (H.μ Δ⁺) # (H.M₁ (H.M₁ (σ̅ σ)) # α)) ≡˘⟨ ap# (H.μ _) (H.M-∘ (H.μ _) (H.M₁ (σ̅ σ)) #ₚ α) ⟩
H.μ Δ⁺ # (H.M₁ (H.μ Δ⁺ ∘ H.M₁ (σ̅ σ)) # α) ∎


T : Functor (Endos SOrdᴴ Fᴴ⟨ Δ ⟩) (Endos SOrdᴹᴰ Fᴹᴰ⟨ Disc Ψ ⟩)
T : Functor (Endos SOrdᴴ (Fᴴ₀ Δ)) (Endos SOrdᴹᴰ Fᴹᴰ⟨ Disc Ψ ⟩)
T = functor
where
functor : Functor (Endos SOrdᴴ Fᴴ⟨ Δ ⟩) (Endos SOrdᴹᴰ Fᴹᴰ⟨ Disc Ψ ⟩)
functor : Functor (Endos SOrdᴴ (Fᴴ₀ Δ)) (Endos SOrdᴹᴰ Fᴹᴰ⟨ Disc Ψ ⟩)
functor .Functor.F₀ _ = tt
functor .Functor.F₁ σ .morphism .hom (α , d) = α , (T′ σ SOrdᴴ.∘ d)
functor .Functor.F₁ σ .morphism .pres-≤[]-equal {α , d1} {β , d2} p =
Expand All @@ -197,17 +193,17 @@ module Mugen.Cat.HierarchyTheory.Universality.EndomorphismEmbedding
functor .Functor.F₁ σ .commutes = trivial!
functor .Functor.F-id = ext λ α d →
refl , λ β →
H.mult.η _ # (H.M₁ (σ̅ SOrdᴴ.id) # (d # β)) ≡⟨ ap (λ e → H.mult.η _ # (H.M₁ e # (d # β))) σ̅-id ⟩
H.mult.η _ # (H.M₁ (H.unit.η _) # (d # β)) ≡⟨ H.left-ident #ₚ _ ⟩
H.μ _ # (H.M₁ (σ̅ SOrdᴴ.id) # (d # β)) ≡⟨ ap (λ e → H.μ _ # (H.M₁ e # (d # β))) σ̅-id ⟩
H.μ _ # (H.M₁ (H.η _) # (d # β)) ≡⟨ H.left-ident #ₚ _ ⟩
d # β ∎
functor .Functor.F-∘ σ δ = ext λ α d →
refl , λ β →
H.mult.η _ # (H.M₁ (σ̅ (σ SOrdᴴ.∘ δ)) # (d # β)) ≡⟨ ap (λ m → H.mult.η _ # (H.M₁ m # (d # β))) (σ̅-∘ σ δ) ⟩
H.mult.η _ # (H.M₁ (H.mult.η _ ∘ H.M₁ (σ̅ σ) ∘ σ̅ δ) # (d # β)) ≡⟨ ap (λ m → H.mult.η _ # (m # (d # β))) (H.M-∘ _ _) ⟩
H.mult.η _ # ((H.M₁ (H.mult.η _) ∘ H.M₁ (H.M₁ (σ̅ σ) ∘ σ̅ δ)) # (d # β)) ≡⟨ ap (λ m → H.mult.η _ # ((H.M₁ (H.mult.η _) ∘ m) # (d # β))) (H.M-∘ _ _) ⟩
H.mult.η _ # (H.M₁ (H.mult.η _) # (H.M₁ (H.M₁ (σ̅ σ)) # (H.M₁ (σ̅ δ) # (d # β)))) ≡⟨ H.mult-assoc #ₚ _ ⟩
H.mult.η _ # (H.mult.η _ # (H.M₁ (H.M₁ (σ̅ σ)) # (H.M₁ (σ̅ δ) # (d # β)))) ≡⟨ ap# (H.mult.η _) (H.mult.is-natural _ _ (σ̅ σ) #ₚ _) ⟩
H.mult.η _ # (H.M₁ (σ̅ σ) # (H.mult.η _ # (H.M₁ (σ̅ δ) # (d # β)))) ∎
H.μ _ # (H.M₁ (σ̅ (σ SOrdᴴ.∘ δ)) # (d # β)) ≡⟨ ap (λ m → H.μ _ # (H.M₁ m # (d # β))) (σ̅-∘ σ δ) ⟩
H.μ _ # (H.M₁ (H.μ _ ∘ H.M₁ (σ̅ σ) ∘ σ̅ δ) # (d # β)) ≡⟨ ap (λ m → H.μ _ # (m # (d # β))) (H.M-∘ _ _) ⟩
H.μ _ # ((H.M₁ (H.μ _) ∘ H.M₁ (H.M₁ (σ̅ σ) ∘ σ̅ δ)) # (d # β)) ≡⟨ ap (λ m → H.μ _ # ((H.M₁ (H.μ _) ∘ m) # (d # β))) (H.M-∘ _ _) ⟩
H.μ _ # (H.M₁ (H.μ _) # (H.M₁ (H.M₁ (σ̅ σ)) # (H.M₁ (σ̅ δ) # (d # β)))) ≡⟨ H.mult-assoc #ₚ _ ⟩
H.μ _ # (H.μ _ # (H.M₁ (H.M₁ (σ̅ σ)) # (H.M₁ (σ̅ δ) # (d # β)))) ≡⟨ ap# (H.μ _) (H.mult.is-natural _ _ (σ̅ σ) #ₚ _) ⟩
H.μ _ # (H.M₁ (σ̅ σ) # (H.μ _ # (H.M₁ (σ̅ δ) # (d # β)))) ∎

--------------------------------------------------------------------------------
-- Faithfulness of T
Expand All @@ -217,9 +213,7 @@ module Mugen.Cat.HierarchyTheory.Universality.EndomorphismEmbedding
T-faithful : ∣ Ψ ∣ → preserves-monos H → is-faithful T
T-faithful pt H-preserves-monos {x} {y} {σ} {δ} p =
free-algebra-hom-path H $ H-preserves-monos ι₁-hom ι₁-monic _ _ $ ext λ α →
σ̅ σ # (ι₁ α) ≡˘⟨ H.right-ident #ₚ _ ⟩
H.mult.η _ # (H.unit.η _ # (σ̅ σ # (ι₁ α))) ≡⟨ ap# (H.mult.η _) (H.unit.is-natural _ _ (σ̅ σ) #ₚ _) ⟩
H.mult.η _ # (H.M₁ (σ̅ σ) # (H.unit.η _ # ι₁ α)) ≡⟨ ap snd (p #ₚ (pt , SOrdᴴ.id)) #ₚ _ ⟩
H.mult.η _ # (H.M₁ (σ̅ δ) # (H.unit.η _ # ι₁ α)) ≡˘⟨ ap# (H.mult.η _) (H.unit.is-natural _ _ (σ̅ δ) #ₚ _) ⟩
H.mult.η _ # (H.unit.η _ # (σ̅ δ # (ι₁ α))) ≡⟨ H.right-ident #ₚ _ ⟩
σ̅ δ # (ι₁ α) ∎
σ̅ σ # ι₁ α ≡˘⟨ μ-η H (σ̅ σ) #ₚ ι₁ α ⟩
H.μ _ # (H.M₁ (σ̅ σ) # (H.η _ # ι₁ α)) ≡⟨ ap snd (p #ₚ (pt , SOrdᴴ.id)) #ₚ _ ⟩
H.μ _ # (H.M₁ (σ̅ δ) # (H.η _ # ι₁ α)) ≡⟨ μ-η H (σ̅ δ) #ₚ ι₁ α ⟩
σ̅ δ # ι₁ α ∎
Loading

0 comments on commit 9a2ab8d

Please sign in to comment.