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

🎨 Tidy up proof that K is strong, add explanations

Browse source
This commit is contained in:
Leon Vatthauer 2023-10-28 13:59:23 +02:00
parent d61a4c8bfa
commit 07dffa087c
Signed by: leonv
SSH key fingerprint: SHA256:G4+ddwoZmhLPRB1agvXzZMXIzkVJ36dUYZXf5NxT+u8
5 changed files with 300 additions and 252 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
.gitignore vendored
View file

@ -3,3 +3,4 @@
*.log
Everything.agda
public/
.direnv

3
index.lagda.md
View file

@ -38,7 +38,8 @@ open import Category.Construction.UniformIterationAlgebras
Existence of free uniform-iteration algebras yields a monad that is of interest to us, we call it **K** and want to show some of it's properties (i.e. that it is strong and an equational lifting monad):
```agda
open import Monad.Instance.K -- TODO move to Monad.Construction.K
open import Monad.Instance.K
open import Monad.Instance.K.Strong
```
Later we will also show that free uniform-iteration algebras coincide with free elgot algebras

1
src/Monad/Instance/Delay/Lemmas.lagda.md
View file

@ -1,5 +1,6 @@
<!--
```agda
{-# OPTIONS --allow-unsolved-metas #-}
open import Level
open import Category.Instance.AmbientCategory
open import Categories.Functor

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

@ -1,58 +1,46 @@
<!--
```agda
{-# OPTIONS --allow-unsolved-metas #-}
open import Level
open import Categories.FreeObjects.Free
open import Categories.Category.Product renaming (Product to CProduct; _⁂_ to _×C_)
open import Categories.Category
open import Categories.Functor.Core
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 Categories.FreeObjects.Free using (FreeObject; FO⇒Functor; FO⇒LAdj)
open import Categories.Functor.Core using (Functor)
open import Categories.Adjoint using (_⊣_)
open import Categories.Adjoint.Properties using (adjoint⇒monad)
open import Categories.Monad using (Monad)
open import Categories.Monad.Relative using () renaming (Monad to RMonad)
open import Category.Instance.AmbientCategory using (Ambient)
open import Categories.NaturalTransformation
open import Categories.Object.Terminal
-- open import Data.Product using (_,_; Σ; Σ-syntax)
open import Categories.Monad.Construction.Kleisli
```
-->
## Summary
In this file I explore the monad ***K*** and its properties:
- [X] *Lemma 16* Definition of the monad
- [ ] *Lemma 16* EilenbergMoore⇒UniformIterationAlgebras (use [crude monadicity theorem](https://agda.github.io/agda-categories/Categories.Adjoint.Monadic.Crude.html))
- [ ] *Proposition 19* ***K*** is strong
- [ ] *Theorem 22* ***K*** is an equational lifting monad
- [ ] *Proposition 23* The Kleisli category of ***K*** is enriched over pointed partial orders and strict monotone maps
- [ ] *Proposition 25* ***K*** is copyable and weakly discardable
- [ ] *Theorem 29* ***K*** is an initial pre-Elgot monad and an initial strong pre-Elgot monad
## Code
# The monad K
```agda
module Monad.Instance.K {o ℓ e} (ambient : Ambient o ℓ e) where
open Ambient ambient
open import Category.Construction.UniformIterationAlgebras ambient
open import Algebra.UniformIterationAlgebra ambient
open import Category.Construction.UniformIterationAlgebras ambient using (Uniform-Iteration-Algebras)
open import Algebra.UniformIterationAlgebra ambient using (Uniform-Iteration-Algebra)
open import Algebra.Properties ambient using (FreeUniformIterationAlgebra; uniformForgetfulF; IsStableFreeUniformIterationAlgebra)
open Equiv
open MR C
open M C
open HomReasoning
```
### *Lemma 16*: definition of monad ***K***
## Definition
The monad is defined by existence of free uniform-iteration algebras.
Since free objects yield and adjunctions, this yields a monad.
```agda
record MonadK : Set (suc o ⊔ suc ℓ ⊔ suc e) where
field
freealgebras : ∀ X → FreeUniformIterationAlgebra X
stable : ∀ X → IsStableFreeUniformIterationAlgebra (freealgebras X)
-- helper for accessing ui-algebras
algebras : ∀ (X : Obj) → Uniform-Iteration-Algebra
algebras X = FreeObject.FX (freealgebras X)
freeF : Functor C Uniform-Iteration-Algebras
freeF = FO⇒Functor uniformForgetfulF freealgebras
@ -60,223 +48,13 @@ module Monad.Instance.K {o ℓ e} (ambient : Ambient o ℓ e) where
adjoint : freeF ⊣ uniformForgetfulF
adjoint = FO⇒LAdj uniformForgetfulF freealgebras
K : Monad C
K = adjoint⇒monad adjoint
```
### *Proposition 19* If the algebras are stable then K is strong
```agda
record MonadKStrong : Set (suc o ⊔ suc ℓ ⊔ suc e) where
field
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 { freealgebras = freealgebras })
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
KStrong = record
{ M = K
; strength = record
{ strengthen = ntHelper (record { η = τ ; commute = commute' })
; identityˡ = identityˡ'
; η-comm = λ {A} {B} → τ-η (A , B)
; μ-η-comm = μ-η-comm'
; strength-assoc = strength-assoc'
}
}
where
open import Agda.Builtin.Sigma
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
private
X = fst P
Y = snd P
τ : X × K₀ Y ⇒ K₀ (X × Y)
τ = η (X × Y) ♯
τ-η : τ ∘ (idC ⁂ η Y) ≈ η (X × Y)
τ-η = sym (♯-law (stable Y) (η (X × Y)))
τ-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
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 ⁂ 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)) # ∎
monadK : Monad C
monadK = adjoint⇒monad adjoint
module monadK = Monad monadK
kleisliK : KleisliTriple C
kleisliK = Monad⇒Kleisli C monadK
module kleisliK = RMonad kleisliK
module K = Functor monadK.F
```

267
src/Monad/Instance/K/Strong.lagda.md Normal file
View file

@ -0,0 +1,267 @@
<!--
```agda
open import Level
open import Categories.FreeObjects.Free
open import Categories.Category.Product using () renaming (Product to CProduct; _⁂_ to _×C_)
open import Data.Product using (_,_; proj₁; proj₂)
open import Categories.Category
open import Categories.Functor.Core
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 Category.Instance.AmbientCategory using (Ambient)
open import Categories.NaturalTransformation
open import Categories.Object.Terminal
import Monad.Instance.K as MIK
```
-->
```agda
module Monad.Instance.K.Strong {o ℓ e} (ambient : Ambient o ℓ e) (MK : MIK.MonadK ambient) where
open Ambient ambient
open import Category.Construction.UniformIterationAlgebras ambient
open import Algebra.UniformIterationAlgebra ambient
open import Algebra.Properties ambient using (FreeUniformIterationAlgebra; uniformForgetfulF; IsStableFreeUniformIterationAlgebra)
open MIK ambient
open MonadK MK
open Equiv
open MR C
open M C
open HomReasoning
```
# The monad K is strong
K is a strong monad with the strength defined as `η ♯`, where ♯ is the operator we get from stability.
Verifying the axioms of strength is straightforward once you know the procedure, since the proofs are all very similar.
For example the proof of `identityˡ` i.e. `K₁ π₂ ∘ τ ≈ π₂` goes as follows:
1. find a morphism `f` such that `K₁ π₂ ∘ τ ≈ f ♯ ≈ π₂`
2. show that `K₁ π₂ ∘ τ` is iteration preserving and satisfies the stabiltiy law
3. show that `π₂` is iteration preserving and satisfies the stabiltiy law
=> by uniqueness of `f ♯` we are done
The following diagram demonstrates this:
<!-- https://q.uiver.app/#q=WzAsNCxbMCwwLCJYXFx0aW1lcyBLWSJdLFsxLDEsIksoWFxcdGltZXMgWSkiXSxbMCwyLCJYXFx0aW1lcyBZIl0sWzIsMCwiS1kiXSxbMCwxLCJcXGV0YV57XFwjfSJdLFsyLDAsImlkXFx0aW1lc1xcZXRhIl0sWzIsMSwiXFxldGEiLDJdLFsxLDMsIktcXHBpXzIiXSxbMCwzLCJcXHBpXzI9KFxcZXRhXFxjaXJjXFxwaV8yKV57XFwjfSJdLFsyLDMsIlxcZXRhXFxjaXJjXFxwaV8yIiwyLHsiY3VydmUiOjR9XV0= -->
<iframe class="quiver-embed" src="https://q.uiver.app/#q=WzAsNCxbMCwwLCJYXFx0aW1lcyBLWSJdLFsxLDEsIksoWFxcdGltZXMgWSkiXSxbMCwyLCJYXFx0aW1lcyBZIl0sWzIsMCwiS1kiXSxbMCwxLCJcXGV0YV57XFwjfSJdLFsyLDAsImlkXFx0aW1lc1xcZXRhIl0sWzIsMSwiXFxldGEiLDJdLFsxLDMsIktcXHBpXzIiXSxbMCwzLCJcXHBpXzI9KFxcZXRhXFxjaXJjXFxwaV8yKV57XFwjfSJdLFsyLDMsIlxcZXRhXFxjaXJjXFxwaV8yIiwyLHsiY3VydmUiOjR9XV0=&embed" width="571" height="432" style="border-radius: 8px; border: none;"></iframe>
```agda
-- we use properties of the kleisli representation as well as the 'normal' monad representation
open kleisliK using (extend)
open monadK using (μ)
KStrength : Strength monoidal monadK
KStrength = record
{ strengthen = ntHelper (record { η = τ ; commute = commute' })
; identityˡ = identityˡ'
; η-comm = λ {A} {B} → τ-η (A , B)
; μ-η-comm = μ-η-comm'
; strength-assoc = strength-assoc'
}
where
open IsStableFreeUniformIterationAlgebra using (♯-law; ♯-preserving; ♯-unique)
open Uniform-Iteration-Algebra using (#-Uniformity; #-Fixpoint; #-resp-≈)
-- some helper definitions to make our life easier
η = λ 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
-- defining τ
module _ (P : Category.Obj (CProduct C C)) where
private
X = proj₁ P
Y = proj₂ P
τ : X × K.₀ Y ⇒ K.₀ (X × Y)
τ = η (X × Y) ♯
τ-η : τ ∘ (idC ⁂ η Y) ≈ η (X × Y)
τ-η = sym (♯-law (stable Y) (η (X × Y)))
τ-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
K₁η : ∀ {X Y} (f : X ⇒ Y) → K.₁ f ∘ η X ≈ η Y ∘ f
K₁η {X} {Y} f = begin
K.₁ f ∘ η X ≈⟨ (sym (F₁⇒extend monadK f)) ⟩∘⟨refl ⟩
extend (η Y ∘ f) ∘ η X ≈⟨ kleisliK.identityʳ ⟩
η Y ∘ f ∎
commute' : ∀ {P₁ : Category.Obj (CProduct C C)} {P₂ : Category.Obj (CProduct C C)} (fg : _[_,_] (CProduct C C) P₁ P₂)
→ τ P₂ ∘ ((proj₁ fg) ⁂ K.₁ (proj₂ fg)) ≈ K.₁ ((proj₁ fg) ⁂ (proj₂ fg)) ∘ τ P₁
commute' {(U , V)} {(W , X)} (f , g) = begin
τ _ ∘ (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 _) uni-helper) ⟩
((τ (W , X) ∘ (f ⁂ K.₁ g) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# ∎
where
uni-helper = 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) ∎
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 monadK π₂)) ⟩∘⟨refl ⟩
extend (η _ ∘ π₂) ∘ η _ ≈⟨ kleisliK.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) uni-helper) ⟩
((π₂ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ∎
where
uni-helper = 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 ∘ π₂ ∎
μ-η-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² monadK.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ˡ monadK.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)) # ∎
strength-assoc' : ∀ {X Y Z} → K.₁ assocˡ ∘ τ (X × Y , Z) ≈ τ (X , Y × Z) ∘ (idC ⁂ τ (Y , Z)) ∘ assocˡ
strength-assoc' {X} {Y} {Z} = begin
K.₁ assocˡ ∘ τ _ ≈⟨ ♯-unique (stable _) (η (X × Y × Z) ∘ assocˡ) (K.₁ assocˡ ∘ τ _) (sym (pullʳ (τ-η _) ○ K₁η _)) comm₁ ⟩
((η (X × Y × Z) ∘ assocˡ) ♯) ≈⟨ sym (♯-unique (stable _) (η (X × Y × Z) ∘ assocˡ) (τ _ ∘ (idC ⁂ τ _) ∘ assocˡ) comm₂ comm₃) ⟩
τ _ ∘ (idC ⁂ τ _) ∘ assocˡ ∎
where
comm₁ : ∀ {A : Obj} (h : A ⇒ K.₀ Z + A) → (K.₁ assocˡ ∘ τ _) ∘ (idC ⁂ h #) ≈ ((K.₁ assocˡ ∘ τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #
comm₁ {A} h = begin
(K.₁ assocˡ ∘ τ _) ∘ (idC ⁂ h #) ≈⟨ pullʳ (τ-comm h) ⟩
K.₁ assocˡ ∘ ((τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# ≈⟨ Uniform-Iteration-Algebra-Morphism.preserves (((freealgebras _) FreeObject.*) _) ⟩
((K.₁ assocˡ +₁ idC) ∘ (τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# ≈⟨ #-resp-≈ (algebras _) (pullˡ (+₁∘+₁ ○ +₁-cong₂ refl identity²)) ⟩
((K.₁ assocˡ ∘ τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ∎
comm₂ : η (X × Y × Z) ∘ assocˡ ≈ (τ _ ∘ (idC ⁂ τ _) ∘ assocˡ) ∘ (idC ⁂ η _)
comm₂ = sym (begin
(τ _ ∘ (idC ⁂ τ _) ∘ assocˡ) ∘ (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ˡ ∎)
comm₃ : ∀ {A : Obj} (h : A ⇒ K.₀ Z + A) → (τ _ ∘ (idC ⁂ τ _) ∘ assocˡ) ∘ (idC ⁂ h #) ≈ ((τ _ ∘ (idC ⁂ τ _) ∘ assocˡ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #
comm₃ {A} h = begin
(τ _ ∘ (idC ⁂ τ _) ∘ assocˡ) ∘ (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ˡ ≈⟨ pullˡ (τ-comm _) ⟩
((τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ (τ (Y , Z) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))) # ∘ assocˡ ≈⟨ sym (#-Uniformity (algebras _) uni-helper) ⟩
((τ _ ∘ (idC ⁂ τ _) ∘ assocˡ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ∎
where
uni-helper : (idC +₁ assocˡ) ∘ (τ _ ∘ (idC ⁂ τ (Y , Z)) ∘ assocˡ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ≈ ((τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ (τ (Y , Z) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))) ∘ assocˡ
uni-helper = begin
(idC +₁ assocˡ) ∘ (τ _ ∘ (idC ⁂ τ (Y , Z)) ∘ assocˡ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ≈⟨ pullˡ +₁∘+₁ ⟩
(idC ∘ τ _ ∘ (idC ⁂ τ (Y , Z)) ∘ assocˡ +₁ assocˡ ∘ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ≈⟨ (+₁-cong₂ identityˡ id-comm) ⟩∘⟨refl ⟩
(τ _ ∘ (idC ⁂ τ (Y , Z)) ∘ assocˡ +₁ idC ∘ assocˡ) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ≈˘⟨ (+₁∘+₁ ○ +₁-cong₂ assoc refl) ⟩∘⟨refl ⟩
((τ _ ∘ (idC ⁂ τ (Y , Z)) +₁ idC) ∘ (assocˡ +₁ assocˡ)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ≈⟨ pullʳ (pullˡ (sym distributeˡ⁻¹-assoc)) ⟩
(τ _ ∘ (idC ⁂ τ (Y , Z)) +₁ idC) ∘ (distributeˡ⁻¹ ∘ (idC ⁂ distributeˡ⁻¹) ∘ assocˡ) ∘ (idC ⁂ h) ≈⟨ refl⟩∘⟨ assoc²' ⟩
(τ _ ∘ (idC ⁂ τ _) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ distributeˡ⁻¹) ∘ assocˡ ∘ (idC ⁂ h) ≈˘⟨ (+₁-cong₂ refl (elimʳ (⟨⟩-unique id-comm id-comm))) ⟩∘⟨refl ⟩
(τ _ ∘ (idC ⁂ τ _) +₁ idC ∘ (idC ⁂ idC)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ distributeˡ⁻¹) ∘ assocˡ ∘ (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ˡ ∘ (idC ⁂ h) ≈⟨ refl⟩∘⟨ ((distribute₁ idC (τ (Y , Z)) idC) ⟩∘⟨refl) ⟩∘⟨refl ⟩
(τ _ +₁ idC) ∘ ((distributeˡ⁻¹ ∘ (idC ⁂ (τ (Y , Z) +₁ idC))) ∘ (idC ⁂ distributeˡ⁻¹)) ∘ assocˡ ∘ (idC ⁂ h) ≈⟨ refl⟩∘⟨ (assoc ○ assoc ○ refl⟩∘⟨ sym-assoc) ⟩
(τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ ((idC ⁂ (τ (Y , Z) +₁ idC)) ∘ (idC ⁂ distributeˡ⁻¹)) ∘ assocˡ ∘ (idC ⁂ h) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (⁂∘⁂ ○ ⁂-cong₂ identity² refl) ⟩∘⟨refl ⟩
(τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ (τ (Y , Z) +₁ idC) ∘ distributeˡ⁻¹) ∘ assocˡ ∘ (idC ⁂ h) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ ⁂-cong₂ (sym (⟨⟩-unique id-comm id-comm)) refl ⟩
(τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ (τ (Y , Z) +₁ idC) ∘ distributeˡ⁻¹) ∘ assocˡ ∘ ((idC ⁂ idC) ⁂ h) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ assocˡ∘⁂ ⟩
(τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ (τ (Y , Z) +₁ idC) ∘ distributeˡ⁻¹) ∘ (idC ⁂ (idC ⁂ h)) ∘ assocˡ ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ assoc ⟩
(τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ ((idC ⁂ (τ (Y , Z) +₁ idC) ∘ distributeˡ⁻¹) ∘ (idC ⁂ (idC ⁂ h))) ∘ assocˡ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⁂∘⁂ ⟩∘⟨refl ⟩
(τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ∘ idC ⁂ ((τ (Y , Z) +₁ idC) ∘ distributeˡ⁻¹) ∘ (idC ⁂ h)) ∘ assocˡ ≈⟨ refl⟩∘⟨ (refl⟩∘⟨ ((⁂-cong₂ identity² assoc) ⟩∘⟨refl) ○ sym-assoc) ○ sym-assoc ⟩
((τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ (τ (Y , Z) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))) ∘ assocˡ ∎
KStrong : StrongMonad {C = C} monoidal
KStrong = record
{ M = monadK
; strength = KStrength
}
```