diff --git a/src/Mugen/Cat/HierarchyTheory/Universality/EndomorphismEmbedding.agda b/src/Mugen/Cat/HierarchyTheory/Universality/EndomorphismEmbedding.agda index 53805c9..5633b1f 100644 --- a/src/Mugen/Cat/HierarchyTheory/Universality/EndomorphismEmbedding.agda +++ b/src/Mugen/Cat/HierarchyTheory/Universality/EndomorphismEmbedding.agda @@ -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⟨Δ⁺⟩→)) @@ -126,16 +129,16 @@ 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) #ₚ α @@ -143,52 +146,45 @@ module Mugen.Cat.HierarchyTheory.Universality.EndomorphismEmbedding 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 = @@ -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 @@ -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 (σ̅ δ) #ₚ ι₁ α ⟩ + σ̅ δ # ι₁ α ∎ diff --git a/src/Mugen/Cat/HierarchyTheory/Universality/HeterogeneousEmbedding.agda b/src/Mugen/Cat/HierarchyTheory/Universality/HeterogeneousEmbedding.agda index 2849f20..091984c 100644 --- a/src/Mugen/Cat/HierarchyTheory/Universality/HeterogeneousEmbedding.agda +++ b/src/Mugen/Cat/HierarchyTheory/Universality/HeterogeneousEmbedding.agda @@ -79,11 +79,14 @@ module Mugen.Cat.HierarchyTheory.Universality.HeterogeneousEmbedding SOrdᴴ = Eilenberg-Moore SOrd H module SOrdᴴ = Cat SOrdᴴ - Fᴴ⟨_⟩ : Poset o o → Algebra SOrd H - Fᴴ⟨_⟩ = Functor.F₀ (Free SOrd H) + Fᴴ₀ : Poset o o → Algebra SOrd H + Fᴴ₀ = Functor.F₀ (Free SOrd H) - Fᴴ⟨Δ₋⟩ : I → Algebra SOrd H - Fᴴ⟨Δ₋⟩ i = Fᴴ⟨ Δ₋ i ⟩ + Fᴴ₁ : {X Y : Poset o o} → Hom X Y → Algebra-hom SOrd H (Fᴴ₀ X) (Fᴴ₀ Y) + Fᴴ₁ = Functor.F₁ (Free SOrd H) + + FᴴΔ₋ : I → Algebra SOrd H + FᴴΔ₋ i = Fᴴ₀ (Δ₋ i) pattern ι n i α = (n , i , α) @@ -98,126 +101,173 @@ module Mugen.Cat.HierarchyTheory.Universality.HeterogeneousEmbedding -- Construction of the functor T -- Section 3.4, Lemma 3.9 - σ̅ : {i j : I} → Algebra-hom SOrd H Fᴴ⟨ Δ₋ i ⟩ Fᴴ⟨ Δ₋ j ⟩ → Hom Δ H⟨Δ⟩ + σ̅ : {i j : I} → Algebra-hom SOrd H (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.unit.η (Δ₋ i) # substᵢ ⌞Δ₋⌟ k=ᵢi α)) - ... | yes _ | suc n | yes _ = H.unit.η Δ # ι (suc n) k α - ... | yes _ | suc n | no _ = H.unit.η Δ # ι n k α - ... | no _ | n | yes _ = H.unit.η Δ # ι (suc n) k α - ... | no _ | n | no _ = H.unit.η Δ # ι n k α + ... | 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.unit.η (Δ₋ i)) .pres-≤[]-equal α≤β - ... | yes reflᵢ | suc n | yes _ = H.unit.η Δ .pres-≤[]-equal (reflᵢ , reflᵢ , α≤β) - ... | yes reflᵢ | suc n | no _ = H⟨Δ⟩.≤[]-map (ap (ι (suc n) k)) $ (H.unit.η Δ ∘ ι-hom n k) .pres-≤[]-equal α≤β - ... | no _ | n | yes _ = H⟨Δ⟩.≤[]-map (ap (ι n k)) $ (H.unit.η Δ ∘ ι-hom (suc n) k) .pres-≤[]-equal α≤β - ... | no _ | n | no _ = H.unit.η Δ .pres-≤[]-equal (reflᵢ , reflᵢ , α≤β) - - abstract - -- "ι0i" means the β-rule for the case "ι 0 i" - - σ̅-ι0i-ext : ∀ {i j k : I} (σ : Algebra-hom SOrd H Fᴴ⟨ Δ₋ i ⟩ Fᴴ⟨ Δ₋ j ⟩) - → (p : k ≡ᵢ i) - → (α : ⌞ Δ₋ k ⌟) - → σ̅ σ # ι 0 k α ≡ H.M₁ (ι-hom 0 j) # (σ # (H.unit.η (Δ₋ i) # substᵢ ⌞Δ₋⌟ p α)) - σ̅-ι0i-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.unit.η (Δ₋ i) # substᵢ ⌞Δ₋⌟ k=ᵢi α)) - ≡⟨ ap# (H.M₁ (ι-hom 0 j) ∘ σ .morphism ∘ H.unit.η (Δ₋ i)) - (λ l → substᵢ ⌞Δ₋⌟ (hlevel 1 k=ᵢi p l) α) ⟩ - H.M₁ (ι-hom 0 j) # (σ # (H.unit.η (Δ₋ i) # substᵢ ⌞Δ₋⌟ p α)) - ∎ - - σ̅-ι0i : ∀ {i j : I} (σ : Algebra-hom SOrd H Fᴴ⟨ Δ₋ i ⟩ Fᴴ⟨ Δ₋ j ⟩) (α : ⌞ Δ₋ i ⌟) - → σ̅ σ # ι 0 i α ≡ H.M₁ (ι-hom 0 j) # (σ # (H.unit.η (Δ₋ i) # α)) - σ̅-ι0i σ = σ̅-ι0i-ext σ reflᵢ - - abstract - H-σ̅-ι0i : ∀ {i j : I} (σ : Algebra-hom SOrd H Fᴴ⟨ Δ₋ i ⟩ Fᴴ⟨ Δ₋ j ⟩) (α : ⌞ H.M₀ (Δ₋ i) ⌟) - → H.mult.η Δ # (H.M₁ (σ̅ σ) # (H.M₁ (ι-hom 0 i) # α)) - ≡ H.M₁ (ι-hom 0 j) # (σ # α) - H-σ̅-ι0i {i = i} {j} σ α = - H.mult.η Δ # (H.M₁ (σ̅ σ) # (H.M₁ (ι-hom 0 i) # α)) - ≡˘⟨ ap# (H.mult.η Δ) $ H.M-∘ (σ̅ σ) (ι-hom 0 i) #ₚ α ⟩ - H.mult.η Δ # (H.M₁ (σ̅ σ ∘ ι-hom 0 i) # α) - ≡⟨ ap (λ m → H.mult.η Δ # (H.M₁ m # α)) $ ext $ σ̅-ι0i σ ⟩ - H.mult.η Δ # (H.M₁ (H.M₁ (ι-hom 0 j) ∘ σ .morphism ∘ H.unit.η (Δ₋ i)) # α) - ≡⟨ ap# (H.mult.η Δ) $ H.M-∘ (H.M₁ (ι-hom 0 j)) (σ .morphism ∘ H.unit.η (Δ₋ i)) #ₚ α ⟩ - H.mult.η Δ # (H.M₁ (H.M₁ (ι-hom 0 j)) # (H.M₁ (σ .morphism ∘ H.unit.η (Δ₋ i)) # α)) - ≡⟨ H.mult.is-natural _ _ (ι-hom 0 j) #ₚ _ ⟩ - H.M₁ (ι-hom 0 j) # (H.mult.η (Δ₋ j) # (H.M₁ (σ .morphism ∘ H.unit.η (Δ₋ i)) # α)) - ≡⟨ ap# (H.M₁ (ι-hom 0 j) ∘ H.mult.η (Δ₋ j)) $ H.M-∘ (σ .morphism) (H.unit.η (Δ₋ i)) #ₚ α ⟩ - H.M₁ (ι-hom 0 j) # (H.mult.η (Δ₋ j) # (H.M₁ (σ .morphism) # (H.M₁ (H.unit.η (Δ₋ i)) # α))) - ≡˘⟨ ap# (H.M₁ (ι-hom 0 j)) $ σ .commutes #ₚ _ ⟩ - H.M₁ (ι-hom 0 j) # (σ # (H.mult.η (Δ₋ i) # (H.M₁ (H.unit.η (Δ₋ i)) # α))) - ≡⟨ ap# (H.M₁ (ι-hom 0 j) ∘ σ .morphism) $ H.left-ident #ₚ _ ⟩ - H.M₁ (ι-hom 0 j) # (σ # α) - ∎ - - abstract - -- "ι1ij" means the β-rule for the case "ι 1 i" - - σ̅-ι1i-ext : ∀ {i j k : I} (σ : Algebra-hom SOrd H Fᴴ⟨ Δ₋ i ⟩ Fᴴ⟨ Δ₋ j ⟩) - → k ≡ᵢ i - → ¬ (k ≡ᵢ j) - → (α : ⌞ Δ₋ k ⌟) - → σ̅ σ # ι (suc n) k α ≡ H.M₁ (ι-hom n k) # (H.unit.η (Δ₋ k) # α) - σ̅-ι0i-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.unit.η (Δ₋ i) # substᵢ ⌞Δ₋⌟ k=ᵢi α)) - ≡⟨ ap# (H.M₁ (ι-hom 0 j) ∘ σ .morphism ∘ H.unit.η (Δ₋ i)) - (λ l → substᵢ ⌞Δ₋⌟ (hlevel 1 k=ᵢi p l) α) ⟩ - H.M₁ (ι-hom 0 j) # (σ # (H.unit.η (Δ₋ i) # substᵢ ⌞Δ₋⌟ p α)) - ∎ - - σ̅-ι0i : ∀ {i j : I} (σ : Algebra-hom SOrd H Fᴴ⟨ Δ₋ i ⟩ Fᴴ⟨ Δ₋ j ⟩) (α : ⌞ Δ₋ i ⌟) - → σ̅ σ # ι 0 i α ≡ H.M₁ (ι-hom 0 j) # (σ # (H.unit.η (Δ₋ i) # α)) - σ̅-ι0i σ = σ̅-ι0i-ext σ reflᵢ - - H-σ̅-ι1ij : ∀ {i j : I} (σ : Algebra-hom SOrd H Fᴴ⟨ Δ₋ i ⟩ Fᴴ⟨ Δ₋ j ⟩) (n : Nat) (α : ⌞ H.M₀ (Δ₋ i) ⌟) (¬p : ¬ (i ≡ᵢ j)) - → H.mult.η Δ # (H.M₁ (σ̅ σ) # (H.M₁ (ι-hom (suc n) i) # α)) - ≡ H.M₁ (ι-hom n j) # (σ # α) - H-σ̅-ι1ij {i = i} {j} σ α = - H.mult.η Δ # (H.M₁ (σ̅ σ) # (H.M₁ (ι-hom 0 i) # α)) - ≡˘⟨ ap# (H.mult.η Δ) $ H.M-∘ (σ̅ σ) (ι-hom 0 i) #ₚ α ⟩ - H.mult.η Δ # (H.M₁ (σ̅ σ ∘ ι-hom 0 i) # α) - ≡⟨ ap (λ m → H.mult.η Δ # (H.M₁ m # α)) $ ext $ σ̅-ι0i σ ⟩ - H.mult.η Δ # (H.M₁ (H.M₁ (ι-hom 0 j) ∘ σ .morphism ∘ H.unit.η (Δ₋ i)) # α) - ≡⟨ ap# (H.mult.η Δ) $ H.M-∘ (H.M₁ (ι-hom 0 j)) (σ .morphism ∘ H.unit.η (Δ₋ i)) #ₚ α ⟩ - H.mult.η Δ # (H.M₁ (H.M₁ (ι-hom 0 j)) # (H.M₁ (σ .morphism ∘ H.unit.η (Δ₋ i)) # α)) - ≡⟨ H.mult.is-natural _ _ (ι-hom 0 j) #ₚ _ ⟩ - H.M₁ (ι-hom 0 j) # (H.mult.η (Δ₋ j) # (H.M₁ (σ .morphism ∘ H.unit.η (Δ₋ i)) # α)) - ≡⟨ ap# (H.M₁ (ι-hom 0 j) ∘ H.mult.η (Δ₋ j)) $ H.M-∘ (σ .morphism) (H.unit.η (Δ₋ i)) #ₚ α ⟩ - H.M₁ (ι-hom 0 j) # (H.mult.η (Δ₋ j) # (H.M₁ (σ .morphism) # (H.M₁ (H.unit.η (Δ₋ i)) # α))) - ≡˘⟨ ap# (H.M₁ (ι-hom 0 j)) $ σ .commutes #ₚ _ ⟩ - H.M₁ (ι-hom 0 j) # (σ # (H.mult.η (Δ₋ i) # (H.M₁ (H.unit.η (Δ₋ i)) # α))) - ≡⟨ ap# (H.M₁ (ι-hom 0 j) ∘ σ .morphism) $ H.left-ident #ₚ _ ⟩ - H.M₁ (ι-hom 0 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} (σ : Algebra-hom SOrd H (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} (σ : Algebra-hom SOrd H (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} (σ : Algebra-hom SOrd H (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} (σ : Algebra-hom SOrd H (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} (σ : Algebra-hom SOrd H (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} (σ : Algebra-hom SOrd H (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)) # α) + ≡⟨ μ-Algebraic H (Fᴴ₁ (ι-hom 0 j)) (σ .morphism ∘ H.η (Δ₋ k)) #ₚ α ⟩ + H.M₁ (ι-hom 0 j) # (H.μ (Δ₋ j) # (H.M₁ (σ .morphism ∘ H.η (Δ₋ k)) # α)) + ≡⟨ ap# (H.M₁ (ι-hom 0 j)) $ μ-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} (σ : Algebra-hom SOrd H (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} (σ : Algebra-hom SOrd H (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} (σ : Algebra-hom SOrd H (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} (σ : Algebra-hom SOrd H (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-lemma : ∀ {i : I} (n : Nat) (k : I) (α : ⌞ Δ₋ k ⌟) → - σ̅ {i = i} SOrdᴴ.id # ι n k α ≡ H.unit.η Δ # ι n k α + σ̅ {i = i} SOrdᴴ.id # ι n k α ≡ H.η Δ # ι n k α σ̅-id-lemma {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 - σ̅-id : ∀ {i : I} → σ̅ {i = i} SOrdᴴ.id ≡ H.unit.η Δ + σ̅-id : ∀ {i : I} → σ̅ {i = i} SOrdᴴ.id ≡ H.η Δ σ̅-id = ext $ σ̅-id-lemma abstract σ̅-∘-ext : ∀ {i j k : I} - (σ : Algebra-hom SOrd H Fᴴ⟨ Δ₋ j ⟩ Fᴴ⟨ Δ₋ k ⟩) - (δ : Algebra-hom SOrd H Fᴴ⟨ Δ₋ i ⟩ Fᴴ⟨ Δ₋ j ⟩) + (σ : Algebra-hom SOrd H (FᴴΔ₋ j) (FᴴΔ₋ k)) + (δ : Algebra-hom SOrd H (FᴴΔ₋ i) (FᴴΔ₋ j)) (n : Nat) (l : I) (α : ⌞Δ₋⌟ l) → σ̅ (σ SOrdᴴ.∘ δ) # ι n l α - ≡ (H.mult.η Δ ∘ H.M₁ (σ̅ σ) ∘ σ̅ δ) # ι n l α - σ̅-∘-ext {i = i} {j} {k} σ δ n l α with l ≡ᵢ? i | n | l ≡ᵢ? j - ... | yes reflᵢ | 0 | _ = - H.M₁ (ι-hom 0 k) # (σ # (δ # (H.unit.η (Δ₋ i) # α))) - ≡˘⟨ H-σ̅-ι0i σ _ ⟩ - H.mult.η Δ # (H.M₁ (σ̅ σ) # (H.M₁ (ι-hom 0 j) # (δ # (H.unit.η (Δ₋ i) # α)))) - ∎ - ... | yes reflᵢ | suc n | yes l=j = {! !} + ≡ (H.μ Δ ∘ H.M₁ (σ̅ σ) ∘ σ̅ δ) # ι n l α + σ̅-∘-ext {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 α diff --git a/src/Mugen/Cat/Monad.agda b/src/Mugen/Cat/Monad.agda index 592a887..b48663e 100644 --- a/src/Mugen/Cat/Monad.agda +++ b/src/Mugen/Cat/Monad.agda @@ -15,26 +15,46 @@ module _ {o r} {C : Precategory o r} (M : Monad C) where open Cat C open Algebra-hom - Free⟨_⟩ : C .Precategory.Ob → Algebra C M - Free⟨_⟩ = Functor.F₀ (Free C M) - - -- Favonia: does this lemma belong to 1lab? - -- - -- NOTE: We can't use any fancy reasoning combinators in this proof, as it really - -- upsets the unifier, as it will fail to unify the homomorphism proofs... - free-algebra-hom-path : ∀ {X Y} {f g : Algebra-hom C M Free⟨ X ⟩ Free⟨ Y ⟩} - → f .morphism ∘ M.unit.η _ ≡ (g .morphism ∘ M.unit.η _) - → f ≡ g - free-algebra-hom-path {f = f} {g = g} p = Algebra-hom-path _ $ - f .morphism ≡⟨ intror M.left-ident ⟩ - f .morphism ∘ M.mult.η _ ∘ M.M₁ (M.unit.η _) ≡⟨ assoc (f .morphism) (M.mult.η _) (M.M₁ (M.unit.η _)) ⟩ - (f .morphism ∘ M.mult.η _) ∘ M.M₁ (M.unit.η _) ≡⟨ ap (_∘ M.M₁ (M.unit.η _)) (f .commutes) ⟩ - (M.mult.η _ ∘ M.M₁ (f .morphism)) ∘ M.M₁ (M.unit.η _) ≡˘⟨ assoc (M.mult.η _) (M.M₁ (f .morphism)) (M.M₁ (M.unit.η _)) ⟩ - M.mult.η _ ∘ M.M₁ (f .morphism) ∘ M.M₁ (M.unit.η _) ≡˘⟨ ap (M.mult.η _ ∘_) (M.M-∘ _ _) ⟩ - M.mult.η _ ∘ M.M₁ (f .morphism ∘ M.unit.η _) ≡⟨ ap (λ ϕ → M.mult.η _ ∘ M.M₁ ϕ) p ⟩ - M.mult.η _ ∘ M.M₁ (g .morphism ∘ M.unit.η _) ≡⟨ ap (M.mult.η _ ∘_) (M.M-∘ _ _) ⟩ - M.mult.η _ ∘ M.M₁ (g .morphism) ∘ M.M₁ (M.unit.η _) ≡⟨ assoc (M.mult.η _) (M.M₁ (g .morphism)) (M.M₁ (M.unit.η _)) ⟩ - (M.mult.η _ ∘ M.M₁ (g .morphism)) ∘ M.M₁ (M.unit.η _) ≡˘⟨ ap (_∘ M.M₁ (M.unit.η _)) (g .commutes) ⟩ - (g .morphism ∘ M.mult.η _) ∘ M.M₁ (M.unit.η _) ≡˘⟨ assoc (g .morphism) (M.mult.η _) (M.M₁ (M.unit.η _)) ⟩ - g .morphism ∘ M.mult.η _ ∘ M.M₁ (M.unit.η _) ≡⟨ elimr M.left-ident ⟩ - g .morphism ∎ + Free₀ : Ob → Algebra C M + Free₀ = Functor.F₀ (Free C M) + + Free₁ : ∀ {X Y} → Hom X Y → Algebra-hom C M (Free₀ X) (Free₀ Y) + Free₁ = Functor.F₁ (Free C M) + + abstract + μ-Algebraic : ∀ {X Y Z} (σ : Algebra-hom C M (Free₀ Y) (Free₀ Z)) (δ : Hom X (M.M₀ Y)) + → M.μ Z ∘ M.M₁ (σ .morphism ∘ δ) ≡ σ .morphism ∘ M.μ Y ∘ M.M₁ δ + μ-Algebraic {X = X} {Y} {Z} σ δ = + M.μ Z ∘ M.M₁ (σ .morphism ∘ δ) + ≡⟨ ap (M.μ Z ∘_) $ M.M-∘ (σ .morphism) δ ⟩ + M.μ Z ∘ M.M₁ (σ .morphism) ∘ (M.M₁ δ) + ≡⟨ assoc (M.μ Z) (M.M₁ (σ .morphism)) (M.M₁ δ) ⟩ + (M.μ Z ∘ M.M₁ (σ .morphism)) ∘ (M.M₁ δ) + ≡˘⟨ ap (_∘ M.M₁ δ) $ σ .commutes ⟩ + (σ .morphism ∘ M.μ Y) ∘ M.M₁ δ + ≡˘⟨ assoc (σ .morphism) (M.μ Y) (M.M₁ δ) ⟩ + σ .morphism ∘ M.μ Y ∘ M.M₁ δ + ∎ + + μ-η : ∀ {X Y} (σ : Hom X (M.M₀ Y)) + → M.μ Y ∘ M.M₁ σ ∘ M.η X ≡ σ + μ-η {X = X} {Y} σ = + M.μ Y ∘ M.M₁ σ ∘ M.η X + ≡˘⟨ ap (M.μ Y ∘_) $ M.unit.is-natural X (M.M₀ Y) σ ⟩ + M.μ Y ∘ M.η (M.M₀ Y) ∘ σ + ≡⟨ assoc (M.μ Y) (M.η (M.M₀ Y)) σ ⟩ + (M.μ Y ∘ M.η (M.M₀ Y)) ∘ σ + ≡⟨ eliml M.right-ident ⟩ + σ + ∎ + + -- Favonia: does this lemma belong to 1lab? + free-algebra-hom-path : ∀ {X Y} {f g : Algebra-hom C M (Free₀ X) (Free₀ Y)} + → f .morphism ∘ M.η _ ≡ (g .morphism ∘ M.η _) → f ≡ g + free-algebra-hom-path {f = f} {g = g} p = Algebra-hom-path _ $ + f .morphism ≡⟨ intror M.left-ident ⟩ + f .morphism ∘ M.μ _ ∘ M.M₁ (M.η _) ≡˘⟨ μ-Algebraic f (M.η _) ⟩ + M.μ _ ∘ M.M₁ (f .morphism ∘ M.η _) ≡⟨ ap (λ ϕ → M.μ _ ∘ M.M₁ ϕ) p ⟩ + M.μ _ ∘ M.M₁ (g .morphism ∘ M.η _) ≡⟨ μ-Algebraic g (M.η _) ⟩ + g .morphism ∘ M.μ _ ∘ M.M₁ (M.η _) ≡⟨ elimr M.left-ident ⟩ + g .morphism ∎