leonv/bsc-leon-vatthauer
1
0
Fork 0
mirror of https://git8.cs.fau.de/theses/bsc-leon-vatthauer.git synced 2024-05-31 07:28:34 +02:00
Code Issues Projects Releases Packages Wiki Activity

Finished strength of K

Browse source
This commit is contained in:
Leon Vatthauer 2023-10-25 18:18:30 +02:00
parent a71045161a
commit 9dfd4145a2
Signed by: leonv
SSH key fingerprint: SHA256:G4+ddwoZmhLPRB1agvXzZMXIzkVJ36dUYZXf5NxT+u8
2 changed files with 246 additions and 50 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

63
src/Category/Instance/AmbientCategory.lagda.md
View file

@ -14,6 +14,9 @@ open import Categories.Category.Cartesian.Monoidal
open import Categories.Category.Cartesian.SymmetricMonoidal using () renaming (symmetric to symm)
open import Categories.Category.Monoidal
open import Categories.Category.Monoidal.Symmetric
open import Categories.Monad
open import Categories.Monad.Construction.Kleisli
open import Categories.Monad.Relative renaming (Monad to RMonad)
open import Categories.Category.Cocartesian using (Cocartesian)
open import Categories.Object.NaturalNumbers.Parametrized using (ParametrizedNNO)
open import Categories.Object.Exponential using (Exponential)
@ -85,7 +88,6 @@ module Category.Instance.AmbientCategory where
[ (idC ⁂ i₁) ∘ swap , (idC ⁂ i₂) ∘ swap ] ∘ distributeʳ⁻¹ ≈⟨ sym (pullˡ []∘+₁) ⟩
distributeˡ ∘ (swap +₁ swap) ∘ distributeʳ⁻¹ ∎)
dstr-law₁ : ∀ {A B C} → distributeˡ⁻¹ {A} {B} {C} ∘ (idC ⁂ i₁) ≈ i₁
dstr-law₁ = (refl⟩∘⟨ (sym inject₁)) ○ (cancelˡ (IsIso.isoˡ isIsoˡ))
dstr-law₂ : ∀ {A B C} → distributeˡ⁻¹ {A} {B} {C} ∘ (idC ⁂ i₂) ≈ i₂
@ -94,6 +96,12 @@ module Category.Instance.AmbientCategory where
dstr-law₃ = (refl⟩∘⟨ (sym inject₁)) ○ (cancelˡ (IsIso.isoˡ isIsoʳ))
dstr-law₄ : ∀ {A B C} → distributeʳ⁻¹ {A} {B} {C} ∘ (i₂ ⁂ idC) ≈ i₂
dstr-law₄ = (refl⟩∘⟨ (sym inject₂)) ○ (cancelˡ (IsIso.isoˡ isIsoʳ))
dstr-law₅ : ∀ {A B C} → (π₂ +₁ π₂) ∘ distributeˡ⁻¹ {A} {B} {C} ≈ π₂
dstr-law₅ = Iso⇒Epi C (IsIso.iso isIsoˡ) ((π₂ +₁ π₂) ∘ distributeˡ⁻¹) π₂ (begin
(((π₂ +₁ π₂) ∘ distributeˡ⁻¹) ∘ distributeˡ) ≈⟨ cancelʳ (IsIso.isoˡ isIsoˡ) ⟩
(π₂ +₁ π₂) ≈˘⟨ []-cong₂ project₂ project₂ ⟩
[ π₂ ∘ _ , π₂ ∘ _ ] ≈˘⟨ ∘[] ⟩
π₂ ∘ distributeˡ ∎)
distribute₂ : ∀ {A B C} → (π₂ +₁ π₂) ∘ distributeˡ⁻¹ {A} {B} {C} ≈ π₂
distribute₂ = sym (begin
π₂ ≈⟨ introʳ (IsIso.isoʳ isIsoˡ) ⟩
@ -101,6 +109,22 @@ module Category.Instance.AmbientCategory where
[ π₂ ∘ ((idC ⁂ i₁)) , π₂ ∘ (idC ⁂ i₂) ] ∘ distributeˡ⁻¹ ≈⟨ ([]-cong₂ π₂∘⁂ π₂∘⁂) ⟩∘⟨refl ⟩
(π₂ +₁ π₂) ∘ distributeˡ⁻¹ ∎)
distributeˡ⁻¹-assoc : ∀ {A B C D : Obj} → distributeˡ⁻¹ ∘ (idC ⁂ distributeˡ⁻¹) ∘ _≅_.to ×-assoc ≈ (_≅_.to ×-assoc +₁ _≅_.to ×-assoc) ∘ distributeˡ⁻¹ {A × B} {C} {D}
distributeˡ⁻¹-assoc {A} {B} {U} {D} = Iso⇒Epi C (IsIso.iso isIsoˡ) (distributeˡ⁻¹ ∘ (idC ⁂ distributeˡ⁻¹) ∘ _≅_.to ×-assoc) ((_≅_.to ×-assoc +₁ _≅_.to ×-assoc) ∘ distributeˡ⁻¹) (begin
(distributeˡ⁻¹ ∘ (idC ⁂ distributeˡ⁻¹) ∘ _≅_.to ×-assoc) ∘ [ idC ⁂ i₁ , idC ⁂ i₂ ] ≈⟨ ∘[] ⟩
[ (distributeˡ⁻¹ ∘ (idC ⁂ distributeˡ⁻¹) ∘ _≅_.to ×-assoc) ∘ (idC ⁂ i₁) , (distributeˡ⁻¹ ∘ (idC ⁂ distributeˡ⁻¹) ∘ _≅_.to ×-assoc) ∘ (idC ⁂ i₂) ] ≈⟨ []-cong₂ (pullʳ (pullʳ ⟨⟩∘)) (pullʳ (pullʳ ⟨⟩∘)) ⟩
[ distributeˡ⁻¹ ∘ (idC ⁂ distributeˡ⁻¹) ∘ ⟨ (π₁ ∘ π₁) ∘ (idC ⁂ i₁) , ⟨ π₂ ∘ π₁ , π₂ ⟩ ∘ (idC ⁂ i₁) ⟩ , distributeˡ⁻¹ ∘ (idC ⁂ distributeˡ⁻¹) ∘ ⟨ (π₁ ∘ π₁) ∘ (idC ⁂ i₂) , ⟨ π₂ ∘ π₁ , π₂ ⟩ ∘ (idC ⁂ i₂) ⟩ ] ≈⟨ []-cong₂ (refl⟩∘⟨ ⁂∘⟨⟩) (refl⟩∘⟨ ⁂∘⟨⟩) ⟩
[ distributeˡ⁻¹ ∘ ⟨ idC ∘ (π₁ ∘ π₁) ∘ (idC ⁂ i₁) , distributeˡ⁻¹ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ∘ (idC ⁂ i₁) ⟩ , distributeˡ⁻¹ ∘ ⟨ idC ∘ (π₁ ∘ π₁) ∘ (idC ⁂ i₂) , distributeˡ⁻¹ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ∘ (idC ⁂ i₂) ⟩ ] ≈⟨ []-cong₂ (refl⟩∘⟨ (⟨⟩-cong₂ identityˡ refl)) (refl⟩∘⟨ (⟨⟩-cong₂ identityˡ refl)) ⟩
[ distributeˡ⁻¹ ∘ ⟨ (π₁ ∘ π₁) ∘ (idC ⁂ i₁) , distributeˡ⁻¹ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ∘ (idC ⁂ i₁) ⟩ , distributeˡ⁻¹ ∘ ⟨ (π₁ ∘ π₁) ∘ (idC ⁂ i₂) , distributeˡ⁻¹ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ∘ (idC ⁂ i₂) ⟩ ] ≈⟨ []-cong₂ (refl⟩∘⟨ (⟨⟩-cong₂ (pullʳ π₁∘⁂) (refl⟩∘⟨ ⟨⟩∘))) (refl⟩∘⟨ ⟨⟩-cong₂ (pullʳ π₁∘⁂) (refl⟩∘⟨ ⟨⟩∘)) ⟩
[ distributeˡ⁻¹ ∘ ⟨ π₁ ∘ idC ∘ π₁ , distributeˡ⁻¹ ∘ ⟨ (π₂ ∘ π₁) ∘ (idC ⁂ i₁) , π₂ ∘ (idC ⁂ i₁) ⟩ ⟩ , distributeˡ⁻¹ ∘ ⟨ π₁ ∘ idC ∘ π₁ , distributeˡ⁻¹ ∘ ⟨ (π₂ ∘ π₁) ∘ (idC ⁂ i₂) , π₂ ∘ (idC ⁂ i₂) ⟩ ⟩ ] ≈⟨ []-cong₂ (refl⟩∘⟨ (⟨⟩-cong₂ (refl⟩∘⟨ identityˡ) (refl⟩∘⟨ (⟨⟩-cong₂ (pullʳ π₁∘⁂) π₂∘⁂)))) (refl⟩∘⟨ (⟨⟩-cong₂ (refl⟩∘⟨ identityˡ) (refl⟩∘⟨ (⟨⟩-cong₂ (pullʳ π₁∘⁂) π₂∘⁂)))) ⟩
[ distributeˡ⁻¹ ∘ ⟨ π₁ ∘ π₁ , distributeˡ⁻¹ ∘ ⟨ π₂ ∘ idC ∘ π₁ , i₁ ∘ π₂ ⟩ ⟩ , distributeˡ⁻¹ ∘ ⟨ π₁ ∘ π₁ , distributeˡ⁻¹ ∘ ⟨ π₂ ∘ idC ∘ π₁ , i₂ ∘ π₂ ⟩ ⟩ ] ≈⟨ []-cong₂ (refl⟩∘⟨ ⟨⟩-cong₂ refl (refl⟩∘⟨ ⟨⟩-cong₂ ((refl⟩∘⟨ identityˡ) ○ sym identityˡ) refl)) (refl⟩∘⟨ ⟨⟩-cong₂ refl (refl⟩∘⟨ ⟨⟩-cong₂ ((refl⟩∘⟨ identityˡ) ○ sym identityˡ) refl)) ⟩
[ distributeˡ⁻¹ ∘ ⟨ π₁ ∘ π₁ , distributeˡ⁻¹ ∘ ⟨ idC ∘ π₂ ∘ π₁ , i₁ ∘ π₂ ⟩ ⟩ , distributeˡ⁻¹ ∘ ⟨ π₁ ∘ π₁ , distributeˡ⁻¹ ∘ ⟨ idC ∘ π₂ ∘ π₁ , i₂ ∘ π₂ ⟩ ⟩ ] ≈˘⟨ []-cong₂ (refl⟩∘⟨ (⟨⟩-cong₂ refl (refl⟩∘⟨ ⁂∘⟨⟩))) (refl⟩∘⟨ (⟨⟩-cong₂ refl (refl⟩∘⟨ ⁂∘⟨⟩))) ⟩
[ distributeˡ⁻¹ ∘ ⟨ π₁ ∘ π₁ , distributeˡ⁻¹ ∘ (idC ⁂ i₁) ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ , distributeˡ⁻¹ ∘ ⟨ π₁ ∘ π₁ , distributeˡ⁻¹ ∘ (idC ⁂ i₂) ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ] ≈⟨ []-cong₂ (refl⟩∘⟨ (⟨⟩-cong₂ (sym identityˡ) (pullˡ dstr-law₁))) (refl⟩∘⟨ (⟨⟩-cong₂ (sym identityˡ) (pullˡ dstr-law₂))) ⟩
[ distributeˡ⁻¹ ∘ ⟨ idC ∘ π₁ ∘ π₁ , i₁ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ , distributeˡ⁻¹ ∘ ⟨ idC ∘ π₁ ∘ π₁ , i₂ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ] ≈˘⟨ []-cong₂ (refl⟩∘⟨ ⁂∘⟨⟩) (refl⟩∘⟨ ⁂∘⟨⟩) ⟩
[ distributeˡ⁻¹ ∘ (idC ⁂ i₁) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ , distributeˡ⁻¹ ∘ (idC ⁂ i₂) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ] ≈⟨ []-cong₂ (pullˡ dstr-law₁) (pullˡ dstr-law₂) ⟩
(_≅_.to ×-assoc +₁ _≅_.to ×-assoc) ≈˘⟨ cancelʳ (IsIso.isoˡ isIsoˡ) ⟩
((_≅_.to ×-assoc +₁ _≅_.to ×-assoc) ∘ distributeˡ⁻¹) ∘ distributeˡ ∎)
module M = M'
module MR = MR'
@ -127,18 +151,8 @@ module Category.Instance.AmbientCategory where
[ ((g +₁ h) ⁂ f) ∘ (i₁ ⁂ idC) , ((g +₁ h) ⁂ f) ∘ (i₂ ⁂ idC) ] ≈˘⟨ ∘[] ⟩
(((g +₁ h) ⁂ f) ∘ distributeʳ) ≈˘⟨ cancelˡ (IsIso.isoʳ isIsoʳ) ⟩∘⟨refl ⟩
(distributeʳ ∘ distributeʳ⁻¹ ∘ ((g +₁ h) ⁂ f)) ∘ distributeʳ ∎))
dstldstr : ∀ {X Y U V} → (distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹ ≈ [ i₁ +₁ i₁ , i₂ +₁ i₂ ] ∘ (distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ (distributeˡ⁻¹ {X + Y} {U} {V})
dstldstr = Iso⇒Epi C (IsIso.iso isIsoˡ) ((distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹) ([ i₁ +₁ i₁ , i₂ +₁ i₂ ] ∘ (distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ distributeˡ⁻¹) (sym (begin
(([ i₁ +₁ i₁ , i₂ +₁ i₂ ] ∘ (distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ distributeˡ⁻¹) ∘ distributeˡ) ≈⟨ pullʳ (cancelʳ (IsIso.isoˡ isIsoˡ)) ⟩
([ i₁ +₁ i₁ , i₂ +₁ i₂ ] ∘ (distributeʳ⁻¹ +₁ distributeʳ⁻¹)) ≈⟨ []∘+₁ ⟩
[ (i₁ +₁ i₁) ∘ distributeʳ⁻¹ , (i₂ +₁ i₂) ∘ distributeʳ⁻¹ ] ≈⟨ {! !} ⟩
{! !} ≈˘⟨ {! !} ⟩
{! !} ≈˘⟨ {! !} ⟩
{! !} ≈˘⟨ {! !} ⟩
{! !} ≈˘⟨ {! !} ⟩
[ ((distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹) ∘ (idC ⁂ i₁) , ((distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹) ∘ (idC ⁂ i₂) ] ≈˘⟨ ∘[] ⟩
(((distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹) ∘ distributeˡ) ∎))
-- TODO replace with use of Iso⇒Epi etc.
iso-epi-from : ∀ {X Y} → (iso : X ≅ Y) → Epi (_≅_.from iso)
iso-epi-from iso = λ f g eq → begin
f ≈⟨ introʳ (_≅_.isoʳ iso) ⟩
@ -151,4 +165,29 @@ module Category.Instance.AmbientCategory where
(f ∘ M'._≅_.to iso ∘ M'._≅_.from iso) ≈⟨ pullˡ eq ⟩
((g ∘ M'._≅_.to iso) ∘ M'._≅_.from iso) ≈⟨ cancelʳ (_≅_.isoˡ iso) ⟩
g ∎
-- TODO should be in agda-categories
Kleisli⇒Monad⇒Kleisli : ∀ (K : KleisliTriple C) {X Y} (f : X ⇒ RMonad.F₀ K Y) → RMonad.extend (Monad⇒Kleisli C (Kleisli⇒Monad C K)) f ≈ RMonad.extend K f
Kleisli⇒Monad⇒Kleisli K f = begin
extend idC ∘ extend (unit ∘ f) ≈⟨ sym kleisli.assoc ⟩
extend (extend idC ∘ unit ∘ f) ≈⟨ extend-≈ (pullˡ kleisli.identityʳ) ⟩
extend (idC ∘ f) ≈⟨ extend-≈ (identityˡ) ⟩
extend f ∎
where
module kleisli = RMonad K
open kleisli using (unit; extend; extend-≈)
Monad⇒Kleisli⇒Monad : ∀ (M : Monad C) {X Y} (f : X ⇒ Monad.F.₀ M Y) → Monad.F.₁ (Kleisli⇒Monad C (Monad⇒Kleisli C M)) f ≈ Monad.F.₁ M f
Monad⇒Kleisli⇒Monad M f = begin
μ.η _ ∘ F.₁ (η.η _ ∘ f) ≈⟨ refl⟩∘⟨ F.homomorphism ⟩
μ.η _ ∘ F.₁ (η.η _) ∘ F.₁ f ≈⟨ cancelˡ monad.identityˡ ⟩
F.₁ f ∎
where
module monad = Monad M
open monad using (F; η; μ)
F₁⇒extend : ∀ (M : Monad C) {X Y} (f : X ⇒ Y) → RMonad.extend (Monad⇒Kleisli C M) (RMonad.unit (Monad⇒Kleisli C M) ∘ f) ≈ Monad.F.₁ M f
F₁⇒extend M f = begin
μ.η _ ∘ F.₁ (η.η _ ∘ f) ≈⟨ refl⟩∘⟨ F.homomorphism ⟩
μ.η _ ∘ F.₁ (η.η _) ∘ F.₁ f ≈⟨ cancelˡ m-identityˡ ⟩
F.₁ f ∎
where open Monad M using (F; η; μ) renaming (identityˡ to m-identityˡ)
```

223
src/Monad/Instance/K.lagda.md
View file

@ -10,6 +10,8 @@ open import Categories.Adjoint
open import Categories.Adjoint.Properties
open import Categories.Monad
open import Categories.Monad.Strong
open import Categories.Monad.Relative renaming (Monad to RMonad)
open import Categories.Monad.Construction.Kleisli
open import Category.Instance.AmbientCategory using (Ambient)
open import Categories.NaturalTransformation
open import Categories.Object.Terminal
@ -35,10 +37,12 @@ In this file I explore the monad ***K*** and its properties:
module Monad.Instance.K {o ℓ e} (ambient : Ambient o ℓ e) where
open Ambient ambient
open import Category.Construction.UniformIterationAlgebras ambient
open import Algebra.UniformIterationAlgebra
open import Algebra.UniformIterationAlgebra ambient
open import Algebra.Properties ambient using (FreeUniformIterationAlgebra; uniformForgetfulF; IsStableFreeUniformIterationAlgebra)
open Equiv
open MR C
open M C
open HomReasoning
```
@ -48,13 +52,13 @@ module Monad.Instance.K {o ℓ e} (ambient : Ambient o ℓ e) where
```agda
record MonadK : Set (suc o ⊔ suc ℓ ⊔ suc e) where
field
algebras : ∀ X → FreeUniformIterationAlgebra X
freealgebras : ∀ X → FreeUniformIterationAlgebra X
freeF : Functor C Uniform-Iteration-Algebras
freeF = FO⇒Functor uniformForgetfulF algebras
freeF = FO⇒Functor uniformForgetfulF freealgebras
adjoint : freeF ⊣ uniformForgetfulF
adjoint = FO⇒LAdj uniformForgetfulF algebras
adjoint = FO⇒LAdj uniformForgetfulF freealgebras
K : Monad C
K = adjoint⇒monad adjoint
@ -65,13 +69,18 @@ module Monad.Instance.K {o ℓ e} (ambient : Ambient o ℓ e) where
```agda
record MonadKStrong : Set (suc o ⊔ suc ℓ ⊔ suc e) where
field
algebras : ∀ X → FreeUniformIterationAlgebra X
stable : ∀ X → IsStableFreeUniformIterationAlgebra (algebras X)
freealgebras : ∀ X → FreeUniformIterationAlgebra X
stable : ∀ X → IsStableFreeUniformIterationAlgebra (freealgebras X)
algebras : ∀ (X : Obj) → Uniform-Iteration-Algebra
algebras X = FreeObject.FX (freealgebras X)
K : Monad C
K = MonadK.K (record { algebras = algebras })
K = MonadK.K (record { freealgebras = freealgebras })
open Monad K using (F)
open Monad K using (F; μ) renaming (identityʳ to m-identityʳ)
module kleisli = RMonad (Monad⇒Kleisli C K)
open kleisli using (extend)
open Functor F using () renaming (F₀ to K₀; F₁ to K₁)
KStrong : StrongMonad {C = C} monoidal
@ -79,47 +88,195 @@ module Monad.Instance.K {o ℓ e} (ambient : Ambient o ℓ e) where
{ M = K
; strength = record
{ strengthen = ntHelper (record { η = τ ; commute = commute' })
; identityˡ = λ {X} → begin
K₁ π₂ ∘ τ _ ≈⟨ refl ⟩
Uniform-Iteration-Algebra-Morphism.h ((algebras (Terminal.⊤ terminal × X) FreeObject.*) (FreeObject.η (algebras X) ∘ π₂)) ∘ τ _ ≈⟨ {! !} ⟩
{! !} ≈⟨ {! !} ⟩
{! !} ≈⟨ {! !} ⟩
π₂ ∎
; η-comm = λ {A} {B} → begin τ _ ∘ (idC ⁂ η (A , B) B) ≈⟨ τ-η (A , B) ⟩ η (A , B) (A × B) ∎
; μ-η-comm = λ {A} {B} → {! !}
; strength-assoc = λ {A} {B} {D} → begin
K₁ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ∘ τ _ ≈⟨ {! !} ⟩
τ _ ∘ (idC ⁂ τ _) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ∎
; identityˡ = identityˡ'
; η-comm = λ {A} {B} → τ-η (A , B)
; μ-η-comm = μ-η-comm'
; strength-assoc = strength-assoc'
}
}
where
open import Agda.Builtin.Sigma
open IsStableFreeUniformIterationAlgebra using (♯-law; ♯-preserving)
open IsStableFreeUniformIterationAlgebra using (♯-law; ♯-preserving; ♯-unique)
open Uniform-Iteration-Algebra using (#-Uniformity; #-Fixpoint; #-resp-≈)
η = λ Z → FreeObject.η (freealgebras Z)
_♯ = λ {A X Y} f → IsStableFreeUniformIterationAlgebra.[_,_]♯ {Y = X} (stable X) {X = A} (algebras Y) f
_# = λ {A} {X} f → Uniform-Iteration-Algebra._# (algebras A) {X = X} f
module _ (P : Category.Obj (CProduct C C)) where
η = λ Z → FreeObject.η (algebras Z)
[_,_,_]♯ = λ {A} X Y f → IsStableFreeUniformIterationAlgebra.[_,_]♯ {Y = X} (stable X) {X = A} Y f
private
X = fst P
Y = snd P
τ : X × K₀ Y ⇒ K₀ (X × Y)
τ = [ Y , FreeObject.FX (algebras (X × Y)) , η (X × Y) ]♯
τ = η (X × Y) ♯
τ-η : τ ∘ (idC ⁂ η Y) ≈ η (X × Y)
τ-η = sym (♯-law (stable Y) (η (X × Y)))
[_,_]# : ∀ (A : Uniform-Iteration-Algebra ambient) {X} → (X ⇒ ((Uniform-Iteration-Algebra.A A) + X)) → (X ⇒ Uniform-Iteration-Algebra.A A)
[ A , f ]# = Uniform-Iteration-Algebra._# A f
τ-comm : ∀ {X Y Z : Obj} (h : Z ⇒ K₀ Y + Z) → τ (X , Y) ∘ (idC ⁂ h #) ≈ ((τ (X , Y) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))#
τ-comm {X} {Y} {Z} h = ♯-preserving (stable Y) (η (X × Y)) h
τ-comm : ∀ {X Y Z : Obj} (h : Z ⇒ K₀ Y + Z) → τ (X , Y) ∘ (idC ⁂ [ FreeObject.FX (algebras Y) , h ]#) ≈ [ FreeObject.FX (algebras (X × Y)) , (τ (X , Y) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ]#
τ-comm {X} {Y} {Z} h = ♯-preserving (stable Y) (η (X , Y) (X × Y)) h
K₁η : ∀ {X Y} (f : X ⇒ Y) → K₁ f ∘ η X ≈ η Y ∘ f
K₁η {X} {Y} f = begin
K₁ f ∘ η X ≈⟨ (sym (F₁⇒extend K f)) ⟩∘⟨refl ⟩
extend (η Y ∘ f) ∘ η X ≈⟨ kleisli.identityʳ ⟩
η Y ∘ f ∎
μ-η-comm' : ∀ {A B} → μ.η _ ∘ K₁ (τ _) ∘ τ (A , K₀ B) ≈ τ _ ∘ (idC ⁂ μ.η _)
μ-η-comm' {A} {B} = begin
μ.η _ ∘ K₁ (τ _) ∘ τ _ ≈⟨ ♯-unique (stable (K₀ B)) (τ (A , B)) (μ.η _ ∘ K₁ (τ _) ∘ τ _) comm₁ comm₂ ⟩
(τ _ ♯) ≈⟨ sym (♯-unique (stable (K₀ B)) (τ (A , B)) (τ _ ∘ (idC ⁂ μ.η _)) (sym (cancelʳ (⁂∘⁂ ○ ⁂-cong₂ identity² m-identityʳ ○ ⟨⟩-unique id-comm id-comm))) comm₃) ⟩
τ _ ∘ (idC ⁂ μ.η _) ∎
where
comm₁ : τ (A , B) ≈ (μ.η _ ∘ K₁ (τ _) ∘ τ _) ∘ (idC ⁂ η _)
comm₁ = sym (begin
(μ.η _ ∘ K₁ (τ _) ∘ τ _) ∘ (idC ⁂ η _) ≈⟨ pullʳ (pullʳ (τ-η _)) ⟩
μ.η _ ∘ K₁ (τ _) ∘ η _ ≈⟨ refl⟩∘⟨ (K₁η (τ (A , B))) ⟩
μ.η _ ∘ η _ ∘ τ _ ≈⟨ cancelˡ m-identityʳ ⟩
τ _ ∎)
comm₂ : ∀ {Z : Obj} (h : Z ⇒ K₀ (K₀ B) + Z) → (μ.η _ ∘ K₁ (τ _) ∘ τ _) ∘ (idC ⁂ h #) ≈ ((μ.η _ ∘ K₁ (τ (A , B)) ∘ τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #
comm₂ {Z} h = begin
(μ.η _ ∘ K₁ (τ _) ∘ τ _) ∘ (idC ⁂ h #) ≈⟨ pullʳ (pullʳ (τ-comm h)) ⟩
μ.η _ ∘ K₁ (τ _) ∘ (((τ (A , K₀ B) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #) ≈⟨ refl⟩∘⟨ (Uniform-Iteration-Algebra-Morphism.preserves (((freealgebras _) FreeObject.*) (η _ ∘ τ _))) ⟩
μ.η _ ∘ ((K₁ (τ _) +₁ idC) ∘ (τ (A , K₀ B) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈⟨ Uniform-Iteration-Algebra-Morphism.preserves (((freealgebras _) FreeObject.*) idC) ⟩
((μ.η _ +₁ idC) ∘ (K₁ (τ _) +₁ idC) ∘ (τ (A , K₀ B) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈⟨ #-resp-≈ (algebras _) (pullˡ +₁∘+₁) ⟩
((μ.η _ ∘ K₁ (τ _) +₁ idC ∘ idC) ∘ (τ (A , K₀ B) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈⟨ #-resp-≈ (algebras _) (pullˡ +₁∘+₁) ⟩
(((μ.η _ ∘ K₁ (τ _)) ∘ τ _ +₁ (idC ∘ idC) ∘ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈⟨ #-resp-≈ (algebras _) ((+₁-cong₂ assoc (cancelʳ identity²)) ⟩∘⟨refl) ⟩
((μ.η _ ∘ K₁ (τ (A , B)) ∘ τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ∎
comm₃ : ∀ {Z : Obj} (h : Z ⇒ K₀ (K₀ B) + Z) → (τ _ ∘ (idC ⁂ μ.η _)) ∘ (idC ⁂ h #) ≈ ((τ _ ∘ (idC ⁂ μ.η _) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #
comm₃ {Z} h = begin
(τ _ ∘ (idC ⁂ μ.η _)) ∘ (idC ⁂ h #) ≈⟨ pullʳ ⁂∘⁂ ⟩
τ _ ∘ (idC ∘ idC ⁂ μ.η _ ∘ h #) ≈⟨ refl⟩∘⟨ (⁂-cong₂ identity² (Uniform-Iteration-Algebra-Morphism.preserves (((freealgebras _) FreeObject.*) idC))) ⟩
τ _ ∘ (idC ⁂ ((μ.η _ +₁ idC) ∘ h) #) ≈⟨ τ-comm ((μ.η B +₁ idC) ∘ h) ⟩
((τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ (μ.η B +₁ idC) ∘ h)) # ≈⟨ #-resp-≈ (algebras _) (refl⟩∘⟨ (refl⟩∘⟨ (⁂-cong₂ (sym identity²) refl ○ sym ⁂∘⁂))) ⟩
((τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ (μ.η B +₁ idC)) ∘ (idC ⁂ h)) # ≈⟨ #-resp-≈ (algebras _) (refl⟩∘⟨ (pullˡ (sym (distribute₁ idC (μ.η B) idC)))) ⟩
((τ _ +₁ idC) ∘ ((idC ⁂ μ.η B +₁ idC ⁂ idC) ∘ distributeˡ⁻¹) ∘ (idC ⁂ h)) # ≈⟨ #-resp-≈ (algebras _) (pullˡ (pullˡ (+₁∘+₁ ○ +₁-cong₂ refl (elimʳ (⟨⟩-unique id-comm id-comm))))) ⟩
(((τ _ ∘ (idC ⁂ μ.η B) +₁ idC) ∘ distributeˡ⁻¹) ∘ (idC ⁂ h)) # ≈⟨ #-resp-≈ (algebras _) assoc ⟩
((τ _ ∘ (idC ⁂ μ.η _) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ∎
module assoc {A} {B} {C} = _≅_ (×-assoc {A} {B} {C})
strength-assoc' : ∀ {X Y Z} → K₁ assoc.to ∘ τ (X × Y , Z) ≈ τ (X , Y × Z) ∘ (idC ⁂ τ (Y , Z)) ∘ assoc.to
strength-assoc' {X} {Y} {Z} = begin
K₁ assoc.to ∘ τ _ ≈⟨ ♯-unique (stable _) (η (X × Y × Z) ∘ assoc.to) (K₁ assoc.to ∘ τ _) (sym (pullʳ (τ-η _) ○ K₁η _)) comm₁ ⟩
((η (X × Y × Z) ∘ assoc.to) ♯) ≈⟨ sym (♯-unique (stable _) (η (X × Y × Z) ∘ assoc.to) (τ _ ∘ (idC ⁂ τ _) ∘ assoc.to) comm₂ comm₃) ⟩
τ _ ∘ (idC ⁂ τ _) ∘ assoc.to ∎
where
comm₁ : ∀ {A : Obj} (h : A ⇒ K₀ Z + A) → (K₁ assoc.to ∘ τ _) ∘ (idC ⁂ h #) ≈ ((K₁ assoc.to ∘ τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #
comm₁ {A} h = begin
(K₁ assoc.to ∘ τ _) ∘ (idC ⁂ h #) ≈⟨ pullʳ (τ-comm h) ⟩
K₁ assoc.to ∘ ((τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# ≈⟨ Uniform-Iteration-Algebra-Morphism.preserves (((freealgebras _) FreeObject.*) _) ⟩
((K₁ assoc.to +₁ idC) ∘ (τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# ≈⟨ #-resp-≈ (algebras _) (pullˡ (+₁∘+₁ ○ +₁-cong₂ refl identity²)) ⟩
((K₁ assoc.to ∘ τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ∎
comm₂ : η (X × Y × Z) ∘ assoc.to ≈ (τ _ ∘ (idC ⁂ τ _) ∘ assoc.to) ∘ (idC ⁂ η _)
comm₂ = sym (begin
(τ _ ∘ (idC ⁂ τ _) ∘ assoc.to) ∘ (idC ⁂ η _) ≈⟨ (refl⟩∘⟨ ⁂∘⟨⟩) ⟩∘⟨refl ⟩
(τ _ ∘ ⟨ idC ∘ π₁ ∘ π₁ , τ _ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ (idC ⁂ η _) ≈⟨ pullʳ ⟨⟩∘ ⟩
τ _ ∘ ⟨ (idC ∘ π₁ ∘ π₁) ∘ (idC ⁂ η _) , (τ _ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩) ∘ (idC ⁂ η _) ⟩ ≈⟨ refl⟩∘⟨ (⟨⟩-cong₂ (identityˡ ⟩∘⟨refl ○ pullʳ π₁∘⁂) (pullʳ ⟨⟩∘)) ⟩
τ _ ∘ ⟨ π₁ ∘ idC ∘ π₁ , τ _ ∘ ⟨ (π₂ ∘ π₁) ∘ (idC ⁂ η _) , π₂ ∘ (idC ⁂ η _) ⟩ ⟩ ≈⟨ refl⟩∘⟨ (⟨⟩-cong₂ (refl⟩∘⟨ identityˡ) (refl⟩∘⟨ (⟨⟩-cong₂ (pullʳ π₁∘⁂) π₂∘⁂))) ⟩
τ _ ∘ ⟨ π₁ ∘ π₁ , τ _ ∘ ⟨ π₂ ∘ idC ∘ π₁ , η _ ∘ π₂ ⟩ ⟩ ≈⟨ refl⟩∘⟨ (⟨⟩-cong₂ (sym identityˡ) (refl⟩∘⟨ ((⟨⟩-cong₂ (sym identityˡ) refl) ○ sym ⁂∘⟨⟩))) ⟩
τ _ ∘ ⟨ idC ∘ π₁ ∘ π₁ , τ _ ∘ (idC ⁂ η _) ∘ ⟨ π₂ ∘ idC ∘ π₁ , π₂ ⟩ ⟩ ≈⟨ refl⟩∘⟨ (⟨⟩-cong₂ refl (pullˡ (τ-η (Y , Z)))) ⟩
τ _ ∘ ⟨ idC ∘ π₁ ∘ π₁ , η _ ∘ ⟨ π₂ ∘ idC ∘ π₁ , π₂ ⟩ ⟩ ≈⟨ refl⟩∘⟨ (sym ⁂∘⟨⟩) ⟩
τ _ ∘ (idC ⁂ η _) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ idC ∘ π₁ , π₂ ⟩ ⟩ ≈⟨ pullˡ (τ-η _) ⟩
η _ ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ idC ∘ π₁ , π₂ ⟩ ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩-cong₂ refl (⟨⟩-cong₂ (refl⟩∘⟨ identityˡ) refl) ⟩
η (X × Y × Z) ∘ assoc.to ∎)
comm₃ : ∀ {A : Obj} (h : A ⇒ K₀ Z + A) → (τ _ ∘ (idC ⁂ τ _) ∘ assoc.to) ∘ (idC ⁂ h #) ≈ ((τ _ ∘ (idC ⁂ τ _) ∘ assoc.to +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #
comm₃ {A} h = begin
(τ _ ∘ (idC ⁂ τ _) ∘ assoc.to) ∘ (idC ⁂ h #) ≈⟨ (refl⟩∘⟨ ⁂∘⟨⟩) ⟩∘⟨refl ⟩
(τ _ ∘ ⟨ idC ∘ π₁ ∘ π₁ , τ _ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ (idC ⁂ h #) ≈⟨ pullʳ ⟨⟩∘ ⟩
τ _ ∘ ⟨ (idC ∘ π₁ ∘ π₁) ∘ (idC ⁂ h #) , (τ _ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩) ∘ (idC ⁂ h #) ⟩ ≈⟨ refl⟩∘⟨ (⟨⟩-cong₂ (identityˡ ⟩∘⟨refl ○ pullʳ π₁∘⁂) (pullʳ ⟨⟩∘)) ⟩
τ _ ∘ ⟨ π₁ ∘ idC ∘ π₁ , τ _ ∘ ⟨ (π₂ ∘ π₁) ∘ (idC ⁂ h #) , π₂ ∘ (idC ⁂ h #) ⟩ ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩-cong₂ (refl⟩∘⟨ identityˡ) (refl⟩∘⟨ (⟨⟩-cong₂ (pullʳ π₁∘⁂) π₂∘⁂)) ⟩
τ _ ∘ ⟨ π₁ ∘ π₁ , τ _ ∘ ⟨ π₂ ∘ idC ∘ π₁ , h # ∘ π₂ ⟩ ⟩ ≈⟨ refl⟩∘⟨ (⟨⟩-cong₂ refl (refl⟩∘⟨ (⟨⟩-cong₂ ((refl⟩∘⟨ identityˡ) ○ sym identityˡ) refl))) ⟩
τ _ ∘ ⟨ π₁ ∘ π₁ , τ _ ∘ ⟨ idC ∘ π₂ ∘ π₁ , h # ∘ π₂ ⟩ ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩-cong₂ refl (refl⟩∘⟨ (sym ⁂∘⟨⟩)) ⟩
τ _ ∘ ⟨ π₁ ∘ π₁ , τ _ ∘ (idC ⁂ h #) ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ≈⟨ refl⟩∘⟨ (⟨⟩-cong₂ (sym identityˡ) (pullˡ (τ-comm h))) ⟩
τ _ ∘ ⟨ idC ∘ π₁ ∘ π₁ , (((τ (Y , Z) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #) ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ≈⟨ refl⟩∘⟨ (sym ⁂∘⟨⟩) ⟩
τ _ ∘ (idC ⁂ ((τ (Y , Z) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #) ∘ assoc.to ≈⟨ pullˡ (τ-comm _) ⟩
((τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ (τ (Y , Z) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))) # ∘ assoc.to ≈⟨ sym (#-Uniformity (algebras _) (begin
(idC +₁ assoc.to) ∘ (τ _ ∘ (idC ⁂ τ (Y , Z)) ∘ assoc.to +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ≈⟨ pullˡ +₁∘+₁ ⟩
(idC ∘ τ _ ∘ (idC ⁂ τ (Y , Z)) ∘ assoc.to +₁ assoc.to ∘ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ≈⟨ (+₁-cong₂ identityˡ id-comm) ⟩∘⟨refl ⟩
(τ _ ∘ (idC ⁂ τ (Y , Z)) ∘ assoc.to +₁ idC ∘ assoc.to) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ≈˘⟨ (+₁∘+₁ ○ +₁-cong₂ assoc refl) ⟩∘⟨refl ⟩
((τ _ ∘ (idC ⁂ τ (Y , Z)) +₁ idC) ∘ (assoc.to +₁ assoc.to)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ≈⟨ pullʳ (pullˡ (sym distributeˡ⁻¹-assoc)) ⟩
(τ _ ∘ (idC ⁂ τ (Y , Z)) +₁ idC) ∘ (distributeˡ⁻¹ ∘ (idC ⁂ distributeˡ⁻¹) ∘ assoc.to) ∘ (idC ⁂ h) ≈⟨ refl⟩∘⟨ assoc²' ⟩
(τ _ ∘ (idC ⁂ τ _) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ distributeˡ⁻¹) ∘ assoc.to ∘ (idC ⁂ h) ≈˘⟨ (+₁-cong₂ refl (elimʳ (⟨⟩-unique id-comm id-comm))) ⟩∘⟨refl ⟩
(τ _ ∘ (idC ⁂ τ _) +₁ idC ∘ (idC ⁂ idC)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ distributeˡ⁻¹) ∘ assoc.to ∘ (idC ⁂ h) ≈˘⟨ assoc ○ assoc ⟩
(((τ _ ∘ (idC ⁂ τ _) +₁ idC ∘ (idC ⁂ idC)) ∘ distributeˡ⁻¹) ∘ (idC ⁂ distributeˡ⁻¹)) ∘ _≅_.to ×-assoc ∘ (idC ⁂ h) ≈˘⟨ pullˡ (pullˡ (pullˡ +₁∘+₁)) ⟩
(τ _ +₁ idC) ∘ ((((idC ⁂ τ _) +₁ (idC ⁂ idC)) ∘ distributeˡ⁻¹) ∘ (idC ⁂ distributeˡ⁻¹)) ∘ assoc.to ∘ (idC ⁂ h) ≈⟨ refl⟩∘⟨ ((distribute₁ idC (τ (Y , Z)) idC) ⟩∘⟨refl) ⟩∘⟨refl ⟩
(τ _ +₁ idC) ∘ ((distributeˡ⁻¹ ∘ (idC ⁂ (τ (Y , Z) +₁ idC))) ∘ (idC ⁂ distributeˡ⁻¹)) ∘ assoc.to ∘ (idC ⁂ h) ≈⟨ refl⟩∘⟨ (assoc ○ assoc ○ refl⟩∘⟨ sym-assoc) ⟩
(τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ ((idC ⁂ (τ (Y , Z) +₁ idC)) ∘ (idC ⁂ distributeˡ⁻¹)) ∘ assoc.to ∘ (idC ⁂ h) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (⁂∘⁂ ○ ⁂-cong₂ identity² refl) ⟩∘⟨refl ⟩
(τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ (τ (Y , Z) +₁ idC) ∘ distributeˡ⁻¹) ∘ assoc.to ∘ (idC ⁂ h) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ ⁂-cong₂ (sym (⟨⟩-unique id-comm id-comm)) refl ⟩
(τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ (τ (Y , Z) +₁ idC) ∘ distributeˡ⁻¹) ∘ assoc.to ∘ ((idC ⁂ idC) ⁂ h) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ assocˡ∘⁂ ⟩
(τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ (τ (Y , Z) +₁ idC) ∘ distributeˡ⁻¹) ∘ (idC ⁂ (idC ⁂ h)) ∘ assoc.to ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ assoc ⟩
(τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ ((idC ⁂ (τ (Y , Z) +₁ idC) ∘ distributeˡ⁻¹) ∘ (idC ⁂ (idC ⁂ h))) ∘ assoc.to ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⁂∘⁂ ⟩∘⟨refl ⟩
(τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ∘ idC ⁂ ((τ (Y , Z) +₁ idC) ∘ distributeˡ⁻¹) ∘ (idC ⁂ h)) ∘ assoc.to ≈⟨ refl⟩∘⟨ (refl⟩∘⟨ ((⁂-cong₂ identity² assoc) ⟩∘⟨refl) ○ sym-assoc) ○ sym-assoc ⟩
((τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ (τ (Y , Z) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))) ∘ assoc.to ∎)) ⟩
((τ _ ∘ (idC ⁂ τ _) ∘ assoc.to +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ∎
commute' : ∀ {P₁ : Category.Obj (CProduct C C)} {P₂ : Category.Obj (CProduct C C)} (fg : _[_,_] (CProduct C C) P₁ P₂)
→ τ P₂ ∘ ((fst fg) ⁂ K₁ (snd fg)) ≈ K₁ ((fst fg) ⁂ (snd fg)) ∘ τ P₁
commute' {(U , V)} {(W , X)} (f , g) = begin
τ _ ∘ (f ⁂ Uniform-Iteration-Algebra-Morphism.h ((algebras V FreeObject.*) (FreeObject.η (algebras X) ∘ g))) ≈⟨ {! !} ⟩
{! !} ≈⟨ {! !} ⟩
{! !} ≈⟨ {! !} ⟩
Uniform-Iteration-Algebra-Morphism.h ((algebras (U × V) FreeObject.*) (FreeObject.η (algebras (W × X)) ∘ (f ⁂ g))) ∘ τ _ ∎
τ _ ∘ (f ⁂ K₁ g) ≈⟨ ♯-unique (stable V) (η (W × X) ∘ (f ⁂ g)) (τ _ ∘ (f ⁂ K₁ g)) comm₁ comm₂ ⟩
(η _ ∘ (f ⁂ g)) ♯ ≈⟨ sym (♯-unique (stable V) (η (W × X) ∘ (f ⁂ g)) (K₁ (f ⁂ g) ∘ τ _) comm₃ comm₄) ⟩
K₁ (f ⁂ g) ∘ τ _ ∎
where
comm₁ : η (W × X) ∘ (f ⁂ g) ≈ (τ (W , X) ∘ (f ⁂ K₁ g)) ∘ (idC ⁂ η V)
comm₁ = sym (begin
(τ (W , X) ∘ (f ⁂ K₁ g)) ∘ (idC ⁂ η V) ≈⟨ pullʳ ⁂∘⁂ ⟩
τ (W , X) ∘ (f ∘ idC ⁂ K₁ g ∘ η V) ≈⟨ refl⟩∘⟨ (⁂-cong₂ id-comm (K₁η g)) ⟩
τ (W , X) ∘ (idC ∘ f ⁂ η X ∘ g) ≈⟨ refl⟩∘⟨ (sym ⁂∘⁂) ⟩
τ (W , X) ∘ (idC ⁂ η X) ∘ (f ⁂ g) ≈⟨ pullˡ (τ-η (W , X)) ⟩
η (W × X) ∘ (f ⁂ g) ∎)
comm₃ : η (W × X) ∘ (f ⁂ g) ≈ (K₁ (f ⁂ g) ∘ τ (U , V)) ∘ (idC ⁂ η V)
comm₃ = sym (begin
(K₁ (f ⁂ g) ∘ τ (U , V)) ∘ (idC ⁂ η V) ≈⟨ pullʳ (τ-η (U , V)) ⟩
K₁ (f ⁂ g) ∘ η (U × V) ≈⟨ K₁η (f ⁂ g) ⟩
η (W × X) ∘ (f ⁂ g) ∎)
comm₂ : ∀ {Z : Obj} (h : Z ⇒ K₀ V + Z) → (τ (W , X) ∘ (f ⁂ K₁ g)) ∘ (idC ⁂ h #) ≈ ((τ (W , X) ∘ (f ⁂ K₁ g) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))#
comm₂ {Z} h = begin
(τ (W , X) ∘ (f ⁂ K₁ g)) ∘ (idC ⁂ h #) ≈⟨ pullʳ ⁂∘⁂ ⟩
τ (W , X) ∘ (f ∘ idC ⁂ K₁ g ∘ (h #)) ≈⟨ refl⟩∘⟨ (⁂-cong₂ id-comm ((Uniform-Iteration-Algebra-Morphism.preserves (((freealgebras _) FreeObject.*) (η X ∘ g))) ○ sym identityʳ)) ⟩
τ (W , X) ∘ (idC ∘ f ⁂ ((K₁ g +₁ idC) ∘ h) # ∘ idC) ≈⟨ refl⟩∘⟨ (sym ⁂∘⁂) ⟩
τ (W , X) ∘ (idC ⁂ ((K₁ g +₁ idC) ∘ h) #) ∘ (f ⁂ idC) ≈⟨ pullˡ (♯-preserving (stable _) (η _) ((K₁ g +₁ idC) ∘ h)) ⟩
((τ (W , X) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ (K₁ g +₁ idC) ∘ h)) # ∘ (f ⁂ idC) ≈⟨ sym (#-Uniformity (algebras _) (begin
(idC +₁ f ⁂ idC) ∘ (τ (W , X) ∘ (f ⁂ K₁ g) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ≈⟨ pullˡ +₁∘+₁ ⟩
(idC ∘ τ (W , X) ∘ (f ⁂ K₁ g) +₁ (f ⁂ idC) ∘ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ≈⟨ (+₁-cong₂ identityˡ id-comm) ⟩∘⟨refl ⟩
(τ (W , X) ∘ (f ⁂ K₁ g) +₁ idC ∘ (f ⁂ idC)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ≈⟨ (sym +₁∘+₁) ⟩∘⟨refl ⟩
((τ (W , X) +₁ idC) ∘ ((f ⁂ K₁ g) +₁ (f ⁂ idC))) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ≈⟨ pullʳ (pullˡ (distribute₁ f (K₁ g) idC)) ⟩
(τ (W , X) +₁ idC) ∘ (distributeˡ⁻¹ ∘ (f ⁂ (K₁ g +₁ idC))) ∘ (idC ⁂ h) ≈⟨ refl⟩∘⟨ (pullʳ (⁂∘⁂ ○ ⁂-cong₂ identityʳ refl)) ⟩
(τ (W , X) +₁ idC) ∘ distributeˡ⁻¹ ∘ (f ⁂ (K₁ g +₁ idC) ∘ h) ≈˘⟨ pullʳ (pullʳ (⁂∘⁂ ○ ⁂-cong₂ identityˡ identityʳ)) ⟩
((τ (W , X) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ (K₁ g +₁ idC) ∘ h)) ∘ (f ⁂ idC) ∎)) ⟩
((τ (W , X) ∘ (f ⁂ K₁ g) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# ∎
comm₄ : ∀ {Z : Obj} (h : Z ⇒ K₀ V + Z) → (K₁ (f ⁂ g) ∘ τ (U , V)) ∘ (idC ⁂ h #) ≈ ((K₁ (f ⁂ g) ∘ τ (U , V) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #
comm₄ {Z} h = begin
(K₁ (f ⁂ g) ∘ τ (U , V)) ∘ (idC ⁂ (h #)) ≈⟨ pullʳ (τ-comm h) ⟩
K₁ (f ⁂ g) ∘ ((τ (U , V) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈⟨ Uniform-Iteration-Algebra-Morphism.preserves (((freealgebras _) FreeObject.*) (η (W × X) ∘ (f ⁂ g))) ⟩
((K₁ (f ⁂ g) +₁ idC) ∘ (τ (U , V) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈⟨ #-resp-≈ (algebras (W × X)) (pullˡ (+₁∘+₁ ○ +₁-cong₂ refl identity²)) ⟩
((K₁ (f ⁂ g) ∘ τ (U , V) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ∎
identityˡ' : ∀ {X : Obj} → K₁ π₂ ∘ τ _ ≈ π₂
identityˡ' {X} = begin
K₁ π₂ ∘ τ _ ≈⟨ ♯-unique (stable X) (η X ∘ π₂) (K₁ π₂ ∘ τ (Terminal.⊤ terminal , X)) comm₁ comm₂ ⟩
(η X ∘ π₂) ♯ ≈⟨ sym (♯-unique (stable X) (η X ∘ π₂) π₂ (sym π₂∘⁂) comm₃) ⟩
π₂ ∎
where
comm₁ : η X ∘ π₂ ≈ (K₁ π₂ ∘ τ (Terminal.⊤ terminal , X)) ∘ (idC ⁂ η X)
comm₁ = sym (begin
(K₁ π₂ ∘ τ (Terminal.⊤ terminal , X)) ∘ (idC ⁂ η X) ≈⟨ pullʳ (τ-η (Terminal.⊤ terminal , X)) ⟩
K₁ π₂ ∘ η (Terminal.⊤ terminal × X) ≈⟨ (sym (F₁⇒extend K π₂)) ⟩∘⟨refl ⟩
extend (η _ ∘ π₂) ∘ η _ ≈⟨ kleisli.identityʳ ⟩
η X ∘ π₂ ∎)
comm₂ : ∀ {Z : Obj} (h : Z ⇒ K₀ X + Z) → (K₁ π₂ ∘ τ (Terminal.⊤ terminal , X)) ∘ (idC ⁂ h # ) ≈ ((K₁ π₂ ∘ τ (Terminal.⊤ terminal , X) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))#
comm₂ {Z} h = begin
(K₁ π₂ ∘ τ _) ∘ (idC ⁂ h #) ≈⟨ pullʳ (♯-preserving (stable X) (η _) h) ⟩
K₁ π₂ ∘ ((τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈⟨ Uniform-Iteration-Algebra-Morphism.preserves ((freealgebras (Terminal.⊤ terminal × X) FreeObject.*) (η X ∘ π₂)) ⟩
((K₁ π₂ +₁ idC) ∘ (τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈⟨ #-resp-≈ (algebras X) (pullˡ (+₁∘+₁ ○ +₁-cong₂ refl identity²)) ⟩
((K₁ π₂ ∘ τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# ∎
comm₃ : ∀ {Z : Obj} (h : Z ⇒ K₀ X + Z) → π₂ ∘ (idC ⁂ h #) ≈ ((π₂ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #
comm₃ {Z} h = begin
π₂ ∘ (idC ⁂ h #) ≈⟨ π₂∘⁂ ⟩
h # ∘ π₂ ≈⟨ sym (#-Uniformity (algebras X) (begin
(idC +₁ π₂) ∘ (π₂ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ≈⟨ pullˡ +₁∘+₁ ⟩
(idC ∘ π₂ +₁ π₂ ∘ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ≈⟨ (+₁-cong₂ identityˡ identityʳ) ⟩∘⟨refl ⟩
(π₂ +₁ π₂) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ≈⟨ pullˡ dstr-law₅ ⟩
π₂ ∘ (idC ⁂ h) ≈⟨ project₂ ⟩
h ∘ π₂ ∎)) ⟩
((π₂ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ∎
```