module Monad.Instance.Delay.Strong {o ℓ e} (ambient : Ambient o ℓ e) (D : DelayM ambient) where
open Ambient ambient
open HomReasoning
open Equiv
open MP C
open MR C
open M C
open F-Coalgebra-Morphism renaming (f to u)
open DelayM D
open Functor
open RMonad kleisli using (extend; extend-≈) renaming (assoc to k-assoc; identityʳ to k-identityʳ)
open Monad monad using (η; μ)
First some facts about strength:
module τ-mod (P : Category.Obj (CProduct C C)) where
private
X = proj₁ P
Y = proj₂ P
open Terminal (coalgebras (X × Y))
τ : X × D₀ Y ⇒ D₀ (X × Y)
τ = u (! {A = record { A = X × D₀ Y ; α = distributeˡ⁻¹ ∘ (idC ⁂ out) }})
τ-law : out ∘ τ ≈ (idC +₁ τ) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out)
τ-law = commutes (! {A = record { A = X × D₀ Y ; α = distributeˡ⁻¹ ∘ (idC ⁂ out) }})
τ-helper : τ ∘ (idC ⁂ out⁻¹) ≈ out⁻¹ ∘ (idC +₁ τ) ∘ distributeˡ⁻¹
τ-helper = begin
τ ∘ (idC ⁂ out⁻¹) ≈⟨ introˡ (_≅_.isoˡ out-≅) ⟩
(out⁻¹ ∘ out) ∘ τ ∘ (idC ⁂ out⁻¹) ≈⟨ pullʳ (pullˡ τ-law) ⟩
out⁻¹ ∘ ((idC +₁ τ) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out)) ∘ (idC ⁂ out⁻¹) ≈⟨ refl⟩∘⟨ (assoc ○ refl⟩∘⟨ assoc) ⟩
out⁻¹ ∘ (idC +₁ τ) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ∘ (idC ⁂ out⁻¹) ≈⟨ refl⟩∘⟨ (refl⟩∘⟨ (elimʳ (⁂∘⁂ ○ (⁂-cong₂ identity² (_≅_.isoʳ out-≅)) ○ ((⟨⟩-cong₂ identityˡ identityˡ) ○ ⁂-η)))) ⟩
out⁻¹ ∘ (idC +₁ τ) ∘ distributeˡ⁻¹ ∎
τ-now : τ ∘ (idC ⁂ now) ≈ now
τ-now = begin
τ ∘ (idC ⁂ now) ≈⟨ refl⟩∘⟨ sym (⁂∘⁂ ○ (⁂-cong₂ identity² refl)) ⟩
τ ∘ (idC ⁂ out⁻¹) ∘ (idC ⁂ i₁) ≈⟨ pullˡ τ-helper ⟩
(out⁻¹ ∘ (idC +₁ τ) ∘ distributeˡ⁻¹) ∘ (idC ⁂ i₁) ≈⟨ pullʳ (pullʳ distributeˡ⁻¹-i₁) ⟩
out⁻¹ ∘ (idC +₁ τ) ∘ i₁ ≈⟨ refl⟩∘⟨ +₁∘i₁ ⟩
out⁻¹ ∘ i₁ ∘ idC ≈⟨ refl⟩∘⟨ identityʳ ⟩
now ∎
▷∘τ : τ ∘ (idC ⁂ ▷) ≈ ▷ ∘ τ
▷∘τ = begin
τ ∘ (idC ⁂ ▷) ≈⟨ refl⟩∘⟨ (sym (⁂∘⁂ ○ ⁂-cong₂ identity² refl)) ⟩
τ ∘ (idC ⁂ out⁻¹) ∘ (idC ⁂ i₂) ≈⟨ pullˡ τ-helper ⟩
(out⁻¹ ∘ (idC +₁ τ) ∘ distributeˡ⁻¹) ∘ (idC ⁂ i₂) ≈⟨ pullʳ (pullʳ distributeˡ⁻¹-i₂) ⟩
out⁻¹ ∘ (idC +₁ τ) ∘ i₂ ≈⟨ refl⟩∘⟨ +₁∘i₂ ⟩
out⁻¹ ∘ i₂ ∘ τ ≈⟨ sym-assoc ⟩
▷ ∘ τ ∎
τ-unique : (t : X × D₀ Y ⇒ D₀ (X × Y)) → (out ∘ t ≈ (idC +₁ t) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out)) → t ≈ τ
τ-unique t t-commutes = sym (!-unique (record { f = t ; commutes = t-commutes }))
open τ-mod
Now we proof strength by coinduction and above properties:
strength : Strength monoidal monad
Strength.strengthen strength = ntHelper (record { η = τ; commute = commute' })
where
commute' : ∀ {P₁ : Category.Obj (CProduct C C)} {P₂ : Category.Obj (CProduct C C)} (fg : _[_,_] (CProduct C C) P₁ P₂)
→ τ P₂ ∘ ((proj₁ fg) ⁂ extend (now ∘ (proj₂ fg))) ≈ extend (now ∘ ((proj₁ fg) ⁂ (proj₂ fg))) ∘ τ P₁
commute' {(U , V)} {(W , X)} (f , g) = by-coinduction ((((f ⁂ g) +₁ idC) ∘ distributeˡ⁻¹) ∘ (idC ⁂ out)) coind₁ coind₂
where
coind₁ : out ∘ τ (W , X) ∘ (f ⁂ extend (now ∘ g)) ≈ (idC +₁ (τ (W , X) ∘ (f ⁂ extend (now ∘ g)))) ∘ ((f ⁂ g +₁ idC) ∘ distributeˡ⁻¹) ∘ (idC ⁂ out)
coind₁ = begin
out ∘ τ (W , X) ∘ (f ⁂ extend (now ∘ g)) ≈⟨ pullˡ (τ-law (W , X)) ⟩
((idC +₁ τ (W , X)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out)) ∘ (f ⁂ extend (now ∘ g)) ≈⟨ pullʳ (pullʳ ⁂∘⁂) ⟩
(idC +₁ τ (W , X)) ∘ distributeˡ⁻¹ ∘ (idC ∘ f ⁂ out ∘ extend (now ∘ g)) ≈⟨ refl⟩∘⟨ (refl⟩∘⟨ (⁂-cong₂ identityˡ (extendlaw (now ∘ g)))) ⟩
(idC +₁ τ (W , X)) ∘ distributeˡ⁻¹ ∘ (f ⁂ [ out ∘ now ∘ g , i₂ ∘ extend (now ∘ g) ] ∘ out) ≈⟨ refl⟩∘⟨ (refl⟩∘⟨ (⁂-cong₂ refl (([]-cong₂ (pullˡ unitlaw) refl) ⟩∘⟨refl))) ⟩
(idC +₁ τ (W , X)) ∘ distributeˡ⁻¹ ∘ (f ⁂ [ i₁ ∘ g , i₂ ∘ extend (now ∘ g) ] ∘ out) ≈⟨ refl⟩∘⟨ (refl⟩∘⟨ (⁂-cong₂ (sym identityʳ) refl)) ⟩
(idC +₁ τ (W , X)) ∘ distributeˡ⁻¹ ∘ (f ∘ idC ⁂ (g +₁ extend (now ∘ g)) ∘ out) ≈⟨ sym (pullʳ (pullʳ ⁂∘⁂)) ⟩
((idC +₁ τ (W , X)) ∘ distributeˡ⁻¹ ∘ (f ⁂ (g +₁ extend (now ∘ g)))) ∘ (idC ⁂ out) ≈⟨ (refl⟩∘⟨ (sym (distributeˡ⁻¹-natural f g (extend (now ∘ g))))) ⟩∘⟨refl ⟩
((idC +₁ τ (W , X)) ∘ ((f ⁂ g) +₁ (f ⁂ extend (now ∘ g))) ∘ distributeˡ⁻¹) ∘ (idC ⁂ out) ≈⟨ (pullˡ +₁∘+₁) ⟩∘⟨refl ⟩
((idC ∘ (f ⁂ g) +₁ τ (W , X) ∘ (f ⁂ extend (now ∘ g))) ∘ distributeˡ⁻¹) ∘ (idC ⁂ out) ≈⟨ sym (((+₁-cong₂ refl identityʳ) ⟩∘⟨refl) ⟩∘⟨refl) ⟩
((idC ∘ (f ⁂ g) +₁ (τ (W , X) ∘ (f ⁂ extend (now ∘ g))) ∘ idC) ∘ distributeˡ⁻¹) ∘ (idC ⁂ out) ≈⟨ sym (pullˡ (pullˡ +₁∘+₁)) ⟩
(idC +₁ (τ (W , X) ∘ (f ⁂ extend (now ∘ g)))) ∘ ((f ⁂ g +₁ idC) ∘ distributeˡ⁻¹) ∘ (idC ⁂ out) ∎
coind₂ : out ∘ extend (now ∘ (f ⁂ g)) ∘ τ (U , V) ≈ (idC +₁ (extend (now ∘ (f ⁂ g)) ∘ τ (U , V))) ∘ (((f ⁂ g) +₁ idC) ∘ distributeˡ⁻¹) ∘ (idC ⁂ out)
coind₂ = begin
out ∘ extend (now ∘ (f ⁂ g)) ∘ τ (U , V) ≈⟨ pullˡ (extendlaw (now ∘ (f ⁂ g))) ⟩
([ out ∘ now ∘ (f ⁂ g) , i₂ ∘ extend (now ∘ (f ⁂ g)) ] ∘ out) ∘ τ (U , V) ≈⟨ (([]-cong₂ (pullˡ unitlaw) refl) ⟩∘⟨refl) ⟩∘⟨refl ⟩
([ i₁ ∘ (f ⁂ g) , i₂ ∘ extend (now ∘ (f ⁂ g)) ] ∘ out) ∘ τ (U , V) ≈⟨ pullʳ (τ-law (U , V)) ⟩
((f ⁂ g) +₁ (extend (now ∘ (f ⁂ g)))) ∘ (idC +₁ τ (U , V)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ sym-assoc ○ sym-assoc ⟩
((((f ⁂ g) +₁ (extend (now ∘ (f ⁂ g)))) ∘ (idC +₁ τ (U , V))) ∘ distributeˡ⁻¹) ∘ (idC ⁂ out) ≈⟨ (+₁∘+₁ ⟩∘⟨refl) ⟩∘⟨refl ⟩
((((f ⁂ g) ∘ idC) +₁ (extend (now ∘ (f ⁂ g)) ∘ τ (U , V))) ∘ distributeˡ⁻¹) ∘ (idC ⁂ out) ≈⟨ sym (((+₁-cong₂ id-comm-sym identityʳ) ⟩∘⟨refl) ⟩∘⟨refl) ⟩
(((idC ∘ (f ⁂ g)) +₁ ((extend (now ∘ (f ⁂ g)) ∘ τ (U , V)) ∘ idC)) ∘ distributeˡ⁻¹) ∘ (idC ⁂ out) ≈⟨ sym (pullˡ (pullˡ +₁∘+₁)) ⟩
(idC +₁ (extend (now ∘ (f ⁂ g)) ∘ τ (U , V))) ∘ (((f ⁂ g) +₁ idC) ∘ distributeˡ⁻¹) ∘ (idC ⁂ out) ∎
Strength.identityˡ strength {X} = by-coinduction ((π₂ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out)) coind₁ coind₂
where
open Terminal terminal using (⊤)
coind₁ : out ∘ extend (now ∘ π₂) ∘ τ (⊤ , X) ≈ (idC +₁ extend (now ∘ π₂) ∘ τ (⊤ , X)) ∘ (π₂ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out)
coind₁ = begin
out ∘ extend (now ∘ π₂) ∘ τ (⊤ , X) ≈⟨ refl⟩∘⟨ (refl⟩∘⟨ (sym identityʳ)) ⟩
out ∘ extend (now ∘ π₂) ∘ τ (⊤ , X) ∘ idC ≈⟨ pullˡ (out-law π₂) ⟩
((π₂ +₁ extend (now ∘ π₂)) ∘ out) ∘ τ (⊤ , X) ∘ idC ≈⟨ pullʳ (pullˡ (τ-law (Terminal.⊤ terminal , X))) ⟩
(π₂ +₁ extend (now ∘ π₂)) ∘ ((idC +₁ τ (⊤ , X)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out)) ∘ idC ≈⟨ refl⟩∘⟨ (pullʳ (assoc ○ sym helper)) ⟩
(π₂ +₁ extend (now ∘ π₂)) ∘ (idC +₁ τ (⊤ , X)) ∘ (⟨ Terminal.! terminal , idC ⟩ +₁ idC) ∘ (π₂ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (pullˡ (+₁∘+₁ ○ +₁-cong₂ (_≅_.isoˡ ⊤×A≅A) identity² ○ []-unique ((identity² ⟩∘⟨refl) ○ id-comm-sym) ((identity² ⟩∘⟨refl) ○ id-comm-sym)) ) ⟩
(π₂ +₁ extend (now ∘ π₂)) ∘ (idC +₁ τ (⊤ , X)) ∘ (idC ∘ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ pullˡ +₁∘+₁ ⟩
(π₂ ∘ idC +₁ extend (now ∘ π₂) ∘ τ (⊤ , X)) ∘ (idC ∘ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ (+₁-cong₂ id-comm refl) ⟩∘⟨refl ⟩
(idC ∘ π₂ +₁ extend (now ∘ π₂) ∘ τ (⊤ , X)) ∘ (idC ∘ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈˘⟨ pullˡ +₁∘+₁ ⟩
(idC +₁ extend (now ∘ π₂)) ∘ (π₂ +₁ τ (⊤ , X)) ∘ (idC ∘ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ refl⟩∘⟨ (refl⟩∘⟨ (elimˡ identity²)) ⟩
(idC +₁ extend (now ∘ π₂)) ∘ (π₂ +₁ τ (⊤ , X)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈˘⟨ refl⟩∘⟨ ((+₁-cong₂ identityˡ identityʳ) ⟩∘⟨refl) ⟩
(idC +₁ extend (now ∘ π₂)) ∘ (idC ∘ π₂ +₁ τ (⊤ , X) ∘ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈˘⟨ pullʳ (pullˡ +₁∘+₁) ⟩
((idC +₁ extend (now ∘ π₂)) ∘ (idC +₁ τ (⊤ , X))) ∘ (π₂ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈˘⟨ (homomorphism (X +-)) ⟩∘⟨refl ⟩
(idC +₁ extend (now ∘ π₂) ∘ τ (⊤ , X)) ∘ (π₂ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ∎
where
helper : (⟨ Terminal.! terminal , idC ⟩ +₁ idC) ∘ (π₂ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈ distributeˡ⁻¹ {Terminal.⊤ terminal} {X} {D₀ X} ∘ (idC ⁂ out) ∘ idC
helper = begin
(⟨ Terminal.! terminal , idC ⟩ +₁ idC) ∘ (π₂ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ pullˡ +₁∘+₁ ⟩
(⟨ Terminal.! terminal , idC ⟩ ∘ π₂ +₁ idC ∘ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ +₁-cong₂ (_≅_.isoˡ ⊤×A≅A) identity² ⟩∘⟨ (refl⟩∘⟨ sym identityʳ) ⟩
(idC +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ∘ idC ≈⟨ elimˡ ([]-unique id-comm-sym id-comm-sym) ⟩
distributeˡ⁻¹ ∘ (idC ⁂ out) ∘ idC ∎
coind₂ : out ∘ π₂ ≈ (idC +₁ π₂) ∘ (π₂ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out)
coind₂ = begin
out ∘ π₂ ≈˘⟨ π₂∘⁂ ⟩
π₂ ∘ (idC ⁂ out) ≈˘⟨ pullˡ distributeˡ⁻¹-π₂ ⟩
(π₂ +₁ π₂) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈˘⟨ (+₁-cong₂ identityˡ identityʳ) ⟩∘⟨refl ⟩
(idC ∘ π₂ +₁ π₂ ∘ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈˘⟨ pullˡ +₁∘+₁ ⟩
(idC +₁ π₂) ∘ (π₂ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ∎
Strength.η-comm strength {X} {Y} = τ-now (X , Y)
Strength.μ-η-comm strength {X} {Y} = by-coinduction ([ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ out)) coind₁ coind₂
where
-- diagram: https://q.uiver.app/#q=WzAsNyxbMCwwLCJYXFx0aW1lcyBERFkiXSxbMiwwLCJEKFhcXHRpbWVzIERZKSJdLFs0LDAsIkREKFhcXHRpbWVzIFkpIl0sWzAsMiwiWFxcdGltZXMgKERZK0REWSkiXSxbMiwyLCJYXFx0aW1lcyBEWSsgWFxcdGltZXMgRERZIl0sWzQsMiwiWFxcdGltZXMgWSsgREQoWFxcdGltZXMgWSkiXSxbMCw0LCJYXFx0aW1lcyBZKyBYXFx0aW1lcyBERFkiXSxbMCwzLCJpZFxcdGltZXMgb3V0IiwyXSxbMCwxLCJcXHRhdSJdLFsxLDIsIlxcdGF1XioiXSxbMyw0LCIoaWQrXFx0YXUpZGlzdCJdLFs0LDUsIltvdXRcXHRhdSxpbnJcXHRhdV4qXSJdLFsyLDUsIm91dCJdLFsxLDRdLFs2LDUsImlkK1xcdGF1XipcXHRhdSIsMl0sWzMsNiwiWyhpZCArIGlkXFx0aW1lcyBub3cpZGlzdCAoaWRcXHRpbWVzIG91dCksaW5yXWRpc3QiLDJdXQ==
id*∘Dτ : extend idC ∘ extend (now ∘ τ (X , Y)) ≈ extend (τ (X , Y))
id*∘Dτ = begin
extend idC ∘ extend (now ∘ τ (X , Y)) ≈⟨ sym k-assoc ⟩
extend (extend idC ∘ now ∘ τ (X , Y)) ≈⟨ extend-≈ (pullˡ k-identityʳ) ⟩
extend (idC ∘ τ (X , Y)) ≈⟨ extend-≈ identityˡ ⟩
extend (τ (X , Y)) ∎
coind₁ : out ∘ extend idC ∘ extend (now ∘ τ (X , Y)) ∘ τ (X , D₀ Y) ≈ (idC +₁ (extend idC ∘ extend (now ∘ τ (X , Y)) ∘ τ (X , D₀ Y))) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ out)
coind₁ = begin
out ∘ extend idC ∘ extend (now ∘ τ (X , Y)) ∘ τ (X , D₀ Y) ≈⟨ refl⟩∘⟨ (pullˡ id*∘Dτ) ⟩
out ∘ extend (τ (X , Y)) ∘ τ (X , D₀ Y) ≈⟨ square ⟩
[ out ∘ τ (X , Y) , i₂ ∘ extend (τ (X , Y)) ] ∘ (idC +₁ τ (X , D₀ Y)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ sym-assoc ○ sym-assoc ○ (assoc ○ tri) ⟩∘⟨refl ⟩
((idC +₁ extend (τ (X , Y)) ∘ τ (X , D₀ Y)) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹) ∘ (idC ⁂ out) ≈⟨ assoc ○ refl⟩∘⟨ assoc ⟩
(idC +₁ (extend (τ (X , Y)) ∘ τ (X , D₀ Y))) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ (+₁-cong₂ refl (sym (pullˡ id*∘Dτ))) ⟩∘⟨refl ⟩
(idC +₁ (extend idC ∘ extend (now ∘ τ (X , Y)) ∘ τ (X , D₀ Y))) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ∎
where
tri : [ out ∘ τ (X , Y) , i₂ ∘ extend (τ (X , Y)) ] ∘ (idC +₁ τ (X , D₀ Y)) ∘ distributeˡ⁻¹ ≈ (idC +₁ extend (τ (X , Y)) ∘ τ (X , D₀ Y)) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹
tri = begin
[ out ∘ τ (X , Y) , i₂ ∘ extend (τ (X , Y)) ] ∘ (idC +₁ τ (X , D₀ Y)) ∘ distributeˡ⁻¹ ≈⟨ pullˡ []∘+₁ ⟩
[ (out ∘ τ (X , Y)) ∘ idC , (i₂ ∘ extend (τ (X , Y))) ∘ τ (X , D₀ Y) ] ∘ distributeˡ⁻¹ ≈⟨ ([]-cong₂ (identityʳ ○ τ-law (X , Y)) assoc) ⟩∘⟨refl ⟩
[ (idC +₁ τ (X , Y)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ∘ extend (τ (X , Y)) ∘ τ (X , D₀ Y) ] ∘ distributeˡ⁻¹ ≈⟨ sym (([]-cong₂ ((+₁-cong₂ refl k-identityʳ) ⟩∘⟨refl) refl) ⟩∘⟨refl) ⟩
[ (idC +₁ extend (τ (X , Y)) ∘ now) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ∘ extend (τ (X , Y)) ∘ τ (X , D₀ Y) ] ∘ distributeˡ⁻¹ ≈⟨ sym (([]-cong₂ ((+₁-cong₂ identity² (pullʳ (τ-now (X , D₀ Y)))) ⟩∘⟨refl) refl) ⟩∘⟨refl) ⟩
[ (idC ∘ idC +₁ (extend (τ (X , Y)) ∘ τ (X , D₀ Y)) ∘ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ∘ extend (τ (X , Y)) ∘ τ (X , D₀ Y) ] ∘ distributeˡ⁻¹ ≈⟨ sym (([]-cong₂ (pullˡ +₁∘+₁) +₁∘i₂) ⟩∘⟨refl) ⟩
[ (idC +₁ extend (τ (X , Y)) ∘ τ (X , D₀ Y)) ∘ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , (idC +₁ extend (τ (X , Y)) ∘ τ (X , D₀ Y)) ∘ i₂ ] ∘ distributeˡ⁻¹ ≈⟨ sym (pullˡ ∘[]) ⟩
(idC +₁ extend (τ (X , Y)) ∘ τ (X , D₀ Y)) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹ ∎
square : out ∘ extend (τ (X , Y)) ∘ τ (X , D₀ Y) ≈ [ out ∘ τ (X , Y) , i₂ ∘ extend (τ (X , Y)) ] ∘ (idC +₁ τ (X , D₀ Y)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out)
square = begin
out ∘ extend (τ (X , Y)) ∘ τ (X , D₀ Y) ≈⟨ pullˡ (extendlaw (τ (X , Y))) ⟩
([ out ∘ τ (X , Y) , i₂ ∘ extend (τ (X , Y)) ] ∘ out) ∘ τ (X , D₀ Y) ≈⟨ pullʳ (τ-law _) ⟩
[ out ∘ τ (X , Y) , i₂ ∘ extend (τ (X , Y)) ] ∘ (idC +₁ τ (X , D₀ Y)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ∎
coind₂ : out ∘ τ (X , Y) ∘ (idC ⁂ extend idC) ≈ (idC +₁ τ (X , Y) ∘ (idC ⁂ extend idC)) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ out)
coind₂ = begin
out ∘ τ (X , Y) ∘ (idC ⁂ extend idC) ≈⟨ pullˡ (τ-law (X , Y)) ⟩
((idC +₁ τ (X , Y)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out)) ∘ (idC ⁂ extend idC) ≈⟨ pullʳ (pullʳ (⁂∘⁂ ○ ⁂-cong₂ identity² refl)) ⟩
(idC +₁ τ (X , Y)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out ∘ extend idC) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⁂-cong₂ refl (extendlaw idC) ⟩
(idC +₁ τ (X , Y)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ [ out ∘ idC , i₂ ∘ extend idC ] ∘ out) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⁂-cong₂ refl (([]-cong₂ identityʳ refl) ⟩∘⟨refl) ⟩
(idC +₁ τ (X , Y)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ [ out , i₂ ∘ extend idC ] ∘ out) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ sym (⁂∘⁂ ○ ⁂-cong₂ identity² refl) ⟩
(idC +₁ τ (X , Y)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ [ out , i₂ ∘ extend idC ]) ∘ (idC ⁂ out) ≈⟨ sym-assoc ○ pullˡ (assoc ○ tri₂) ⟩
((idC +₁ τ (X , Y) ∘ (idC ⁂ extend idC)) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹) ∘ (idC ⁂ out) ≈⟨ assoc ○ refl⟩∘⟨ assoc ⟩
(idC +₁ τ (X , Y) ∘ (idC ⁂ extend idC)) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ∎
where
tri₂' : (idC +₁ τ (X , Y)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ [ out , i₂ ∘ extend idC ]) ∘ [ (idC ⁂ i₁) , (idC ⁂ i₂) ] ≈ (idC +₁ τ (X , Y) ∘ (idC ⁂ extend idC)) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹ ∘ distributeˡ
tri₂' = begin
(idC +₁ τ (X , Y)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ [ out , i₂ ∘ extend idC ]) ∘ [ (idC ⁂ i₁) , (idC ⁂ i₂) ] ≈⟨ refl⟩∘⟨ (refl⟩∘⟨ ∘[]) ⟩
(idC +₁ τ (X , Y)) ∘ distributeˡ⁻¹ ∘ [ (idC ⁂ [ out , i₂ ∘ extend idC ]) ∘ (idC ⁂ i₁) , (idC ⁂ [ out , i₂ ∘ extend idC ]) ∘ (idC ⁂ i₂) ] ≈⟨ refl⟩∘⟨ refl⟩∘⟨ []-cong₂ ⁂∘⁂ ⁂∘⁂ ⟩
(idC +₁ τ (X , Y)) ∘ distributeˡ⁻¹ ∘ [ (idC ∘ idC ⁂ [ out , i₂ ∘ extend idC ] ∘ i₁) , (idC ∘ idC ⁂ [ out , i₂ ∘ extend idC ] ∘ i₂) ] ≈⟨ refl⟩∘⟨ refl⟩∘⟨ []-cong₂ (⁂-cong₂ identity² inject₁) (⁂-cong₂ identity² inject₂) ⟩
(idC +₁ τ (X , Y)) ∘ distributeˡ⁻¹ ∘ [ idC ⁂ out , idC ⁂ i₂ ∘ extend idC ] ≈⟨ refl⟩∘⟨ ∘[] ⟩
(idC +₁ τ (X , Y)) ∘ [ distributeˡ⁻¹ ∘ (idC ⁂ out) , distributeˡ⁻¹ ∘ (idC ⁂ i₂ ∘ extend idC) ] ≈⟨ ∘[] ⟩
[ (idC +₁ τ (X , Y)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , (idC +₁ τ (X , Y)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ i₂ ∘ extend idC) ] ≈⟨ sym ([]-cong₂ refl (pullʳ (pullʳ (⁂∘⁂ ○ ⁂-cong₂ identity² refl)))) ⟩
[ (idC +₁ τ (X , Y)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , ((idC +₁ τ (X , Y)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ i₂)) ∘ (idC ⁂ extend idC) ] ≈⟨ []-cong₂ refl ((refl⟩∘⟨ distributeˡ⁻¹-i₂) ⟩∘⟨refl) ⟩
[ (idC +₁ τ (X , Y)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , ((idC +₁ τ (X , Y)) ∘ i₂) ∘ (idC ⁂ extend idC) ] ≈⟨ []-cong₂ refl (pushˡ +₁∘i₂) ⟩
[ (idC +₁ τ (X , Y)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ∘ τ (X , Y) ∘ (idC ⁂ extend idC) ] ≈⟨ []-cong₂ ((+₁-cong₂ refl (introʳ (⟨⟩-unique id-comm (id-comm ○ (sym k-identityʳ) ⟩∘⟨refl)))) ⟩∘⟨refl) refl ⟩
[ (idC +₁ τ (X , Y) ∘ (idC ⁂ extend idC ∘ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ∘ τ (X , Y) ∘ (idC ⁂ extend idC) ] ≈⟨ []-cong₂ ((sym (+₁-cong₂ refl (refl⟩∘⟨ (⁂∘⁂ ○ ⁂-cong₂ identity² refl)))) ⟩∘⟨refl) refl ⟩
[ (idC +₁ τ (X , Y) ∘ (idC ⁂ extend idC) ∘ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ∘ τ (X , Y) ∘ (idC ⁂ extend idC) ] ≈⟨ sym ([]-cong₂ (pullˡ (+₁∘+₁ ○ +₁-cong₂ identity² assoc)) +₁∘i₂) ⟩
[ (idC +₁ τ (X , Y) ∘ (idC ⁂ extend idC)) ∘ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , (idC +₁ τ (X , Y) ∘ (idC ⁂ extend idC)) ∘ i₂ ] ≈⟨ sym ∘[] ⟩
(idC +₁ τ (X , Y) ∘ (idC ⁂ extend idC)) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ≈⟨ sym (refl⟩∘⟨ (elimʳ (IsIso.isoˡ isIsoˡ))) ⟩
(idC +₁ τ (X , Y) ∘ (idC ⁂ extend idC)) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹ ∘ distributeˡ ∎
tri₂ : (idC +₁ τ (X , Y)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ [ out , i₂ ∘ extend idC ]) ≈ (idC +₁ τ (X , Y) ∘ (idC ⁂ extend idC)) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹
tri₂ = Iso⇒Epi
(IsIso.iso isIsoˡ)
((idC +₁ τ (X , Y)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ [ out , i₂ ∘ extend idC ]))
((idC +₁ τ (X , Y) ∘ (idC ⁂ extend idC)) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹)
(assoc ○ refl⟩∘⟨ assoc ○ tri₂' ○ sym-assoc ○ sym-assoc ○ assoc ⟩∘⟨refl)
Strength.strength-assoc strength {X} {Y} {Z} = by-coinduction ((⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out)) coind₁ coind₂
where
coind₁ : out ∘ extend (now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ τ (X × Y , Z) ≈ (idC +₁ extend (now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ τ (X × Y , Z)) ∘ (⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out)
coind₁ = begin
out ∘ extend (now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ τ (X × Y , Z) ≈⟨ pullˡ (extendlaw (now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩)) ⟩
([ out ∘ now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ , i₂ ∘ extend (now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ] ∘ out) ∘ τ (X × Y , Z) ≈⟨ pullʳ (τ-law (X × Y , Z)) ⟩
[ out ∘ now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ , i₂ ∘ extend (now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ] ∘ (idC +₁ τ (X × Y , Z)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ ([]-cong₂ (pullˡ unitlaw) refl) ⟩∘⟨refl ⟩
(⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ +₁ extend (now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩)) ∘ (idC +₁ τ (X × Y , Z)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ pullˡ +₁∘+₁ ⟩
(⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ∘ idC +₁ extend (now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ τ (X × Y , Z)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ (+₁-cong₂ id-comm (sym identityʳ)) ⟩∘⟨refl ⟩
(idC ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ +₁ (extend (now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ τ (X × Y , Z)) ∘ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ sym (pullˡ +₁∘+₁) ⟩
(idC +₁ extend (now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ τ (X × Y , Z)) ∘ (⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ∎
coind₂ : out ∘ τ (X , Y × Z) ∘ (idC ⁂ τ (Y , Z)) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ≈ (idC +₁ τ (X , Y × Z) ∘ (idC ⁂ τ (Y , Z)) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ (⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out)
coind₂ = begin
out ∘ τ (X , Y × Z) ∘ (idC ⁂ τ (Y , Z)) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ≈⟨ pullˡ (τ-law (X , Y × Z)) ⟩
((idC +₁ τ (X , Y × Z)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out)) ∘ (idC ⁂ τ (Y , Z)) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ≈⟨ pullʳ (pullˡ (pullʳ ⁂∘⁂)) ⟩
(idC +₁ τ (X , Y × Z)) ∘ (distributeˡ⁻¹ ∘ (idC ∘ idC ⁂ out ∘ τ (Y , Z))) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ≈⟨ refl⟩∘⟨ assoc ⟩
(idC +₁ τ (X , Y × Z)) ∘ distributeˡ⁻¹ ∘ (idC ∘ idC ⁂ out ∘ τ (Y , Z)) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ≈˘⟨ refl⟩∘⟨ (refl⟩∘⟨ (⁂-cong₂ identityʳ (assoc ○ sym (τ-law (Y , Z)))) ⟩∘⟨refl) ⟩
(idC +₁ τ (X , Y × Z)) ∘ distributeˡ⁻¹ ∘ ((idC ∘ idC) ∘ idC ⁂ ((idC +₁ τ (Y , Z)) ∘ distributeˡ⁻¹) ∘ (idC ⁂ out)) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ≈⟨ sym (refl⟩∘⟨ (pullʳ (pullˡ ⁂∘⁂ ○ pullˡ ⁂∘⁂))) ⟩
(idC +₁ τ (X , Y × Z)) ∘ (distributeˡ⁻¹ ∘ (idC ⁂ (idC +₁ τ (Y , Z)))) ∘ (idC ⁂ distributeˡ⁻¹) ∘ (idC ⁂ (idC ⁂ out)) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ≈⟨ refl⟩∘⟨ (refl⟩∘⟨ (refl⟩∘⟨ helper₁)) ⟩
(idC +₁ τ (X , Y × Z)) ∘ (distributeˡ⁻¹ ∘ (idC ⁂ (idC +₁ τ (Y , Z)))) ∘ (idC ⁂ distributeˡ⁻¹) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ∘ (idC ⁂ out) ≈⟨ refl⟩∘⟨ (helper₂ ⟩∘⟨refl) ⟩
(idC +₁ τ (X , Y × Z)) ∘ ((idC +₁ (idC ⁂ τ (Y , Z))) ∘ distributeˡ⁻¹) ∘ (idC ⁂ distributeˡ⁻¹) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ∘ (idC ⁂ out) ≈⟨ refl⟩∘⟨ (assoc ○ refl⟩∘⟨ sym assoc²') ⟩
(idC +₁ τ (X , Y × Z)) ∘ (idC +₁ (idC ⁂ τ (Y , Z))) ∘ (distributeˡ⁻¹ ∘ (idC ⁂ distributeˡ⁻¹) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ (idC ⁂ out) ≈⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ identity² refl) ⟩
(idC +₁ τ (X , Y × Z) ∘ (idC ⁂ τ (Y , Z))) ∘ (distributeˡ⁻¹ ∘ (idC ⁂ distributeˡ⁻¹) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ (idC ⁂ out) ≈⟨ refl⟩∘⟨ (helper₃ ⟩∘⟨refl) ⟩
(idC +₁ τ (X , Y × Z) ∘ (idC ⁂ τ (Y , Z))) ∘ ((⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ +₁ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ distributeˡ⁻¹) ∘ (idC ⁂ out) ≈⟨ assoc²'' ⟩
((idC +₁ τ (X , Y × Z) ∘ (idC ⁂ τ (Y , Z))) ∘ (⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ +₁ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ sym ((+₁-cong₂ refl (identityʳ ○ sym-assoc) ○ sym +₁∘+₁) ⟩∘⟨refl) ⟩
(idC ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ +₁ (τ (X , Y × Z) ∘ (idC ⁂ τ (Y , Z)) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ sym (pullˡ +₁∘+₁) ⟩
(idC +₁ τ (X , Y × Z) ∘ (idC ⁂ τ (Y , Z)) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ (⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ∎
where
helper₁ : (idC ⁂ (idC ⁂ out)) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ≈ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ∘ (idC {X × Y} ⁂ out {Z})
helper₁ = begin
(idC ⁂ (idC ⁂ out)) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ≈⟨ ⁂∘⟨⟩ ⟩
⟨ idC ∘ π₁ ∘ π₁ , (idC ⁂ out) ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ≈⟨ ⟨⟩-cong₂ identityˡ ⁂∘⟨⟩ ⟩
⟨ π₁ ∘ π₁ , ⟨ idC ∘ π₂ ∘ π₁ , out ∘ π₂ ⟩ ⟩ ≈⟨ ⟨⟩-cong₂ refl (⟨⟩-cong₂ identityˡ refl) ⟩
⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , out ∘ π₂ ⟩ ⟩ ≈⟨ sym (⟨⟩-cong₂ refl (⟨⟩-cong₂ (refl⟩∘⟨ identityˡ) refl)) ⟩
⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ idC ∘ π₁ , out ∘ π₂ ⟩ ⟩ ≈⟨ sym (⟨⟩-cong₂ (refl⟩∘⟨ identityˡ) (⟨⟩-cong₂ (pullʳ π₁∘⁂) π₂∘⁂)) ⟩
⟨ π₁ ∘ idC ∘ π₁ , ⟨ (π₂ ∘ π₁) ∘ (idC {X × Y} ⁂ out {Z}) , π₂ ∘ (idC {X × Y} ⁂ out {Z}) ⟩ ⟩ ≈⟨ sym (⟨⟩-cong₂ (pullʳ project₁) ⟨⟩∘) ⟩
⟨ (π₁ ∘ π₁) ∘ (idC {X × Y} ⁂ out {Z}) , ⟨ π₂ ∘ π₁ , π₂ ⟩ ∘ (idC {X × Y} ⁂ out {Z}) ⟩ ≈⟨ sym ⟨⟩∘ ⟩
⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ∘ (idC {X × Y} ⁂ out {Z}) ∎
helper₂ : distributeˡ⁻¹ ∘ (idC ⁂ (idC +₁ τ (Y , Z))) ≈ (idC +₁ (idC ⁂ τ (Y , Z))) ∘ distributeˡ⁻¹
helper₂ = sym (distributeˡ⁻¹-natural idC idC (τ (Y , Z))) ○ (+₁-cong₂ (⟨⟩-unique id-comm id-comm) refl) ⟩∘⟨refl
helper₃ : distributeˡ⁻¹ ∘ (idC ⁂ distributeˡ⁻¹) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ≈ (⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ +₁ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ distributeˡ⁻¹
helper₃ = sym (begin
(⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ +₁ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ distributeˡ⁻¹ ≈⟨ introˡ (IsIso.isoˡ isIsoˡ) ⟩
(distributeˡ⁻¹ ∘ distributeˡ) ∘ (⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ +₁ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ distributeˡ⁻¹ ≈⟨ pullʳ (pullˡ []∘+₁) ⟩
distributeˡ⁻¹ ∘ [ (idC ⁂ i₁) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ , (idC ⁂ i₂) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ] ∘ distributeˡ⁻¹ ≈⟨ refl⟩∘⟨ (([]-cong₂ ⁂∘⟨⟩ ⁂∘⟨⟩) ⟩∘⟨refl) ⟩
distributeˡ⁻¹ ∘ [ ⟨ idC ∘ π₁ ∘ π₁ , i₁ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ , ⟨ idC ∘ π₁ ∘ π₁ , i₂ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ] ∘ distributeˡ⁻¹ ≈⟨ refl⟩∘⟨ []-cong₂ (⟨⟩-cong₂ identityˡ (pushˡ (sym distributeˡ⁻¹-i₁))) (⟨⟩-cong₂ identityˡ ((pushˡ (sym distributeˡ⁻¹-i₂)))) ⟩∘⟨refl ⟩
distributeˡ⁻¹ ∘ [ ⟨ π₁ ∘ π₁ , distributeˡ⁻¹ ∘ (idC ⁂ i₁) ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ , ⟨ π₁ ∘ π₁ , distributeˡ⁻¹ ∘ (idC ⁂ i₂) ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ] ∘ distributeˡ⁻¹ ≈⟨ sym (refl⟩∘⟨ []-cong₂ (⟨⟩-cong₂ refl (refl⟩∘⟨ (⟨⟩-cong₂ (refl⟩∘⟨ identityˡ ○ sym identityˡ) refl ○ sym ⁂∘⟨⟩))) (⟨⟩-cong₂ refl (refl⟩∘⟨ (⟨⟩-cong₂ (refl⟩∘⟨ identityˡ ○ sym identityˡ) refl ○ sym ⁂∘⟨⟩))) ⟩∘⟨refl) ⟩
distributeˡ⁻¹ ∘ [ ⟨ π₁ ∘ π₁ , distributeˡ⁻¹ ∘ ⟨ π₂ ∘ idC ∘ π₁ , i₁ ∘ π₂ ⟩ ⟩ , ⟨ π₁ ∘ π₁ , distributeˡ⁻¹ ∘ ⟨ π₂ ∘ idC ∘ π₁ , i₂ ∘ π₂ ⟩ ⟩ ] ∘ distributeˡ⁻¹ ≈⟨ sym (refl⟩∘⟨ []-cong₂ (⟨⟩-cong₂ (identityˡ ○ refl⟩∘⟨ identityˡ) (refl⟩∘⟨ (⟨⟩-cong₂ (pullʳ π₁∘⁂) π₂∘⁂))) (⟨⟩-cong₂ (identityˡ ○ refl⟩∘⟨ identityˡ) (refl⟩∘⟨ (⟨⟩-cong₂ (pullʳ π₁∘⁂) π₂∘⁂))) ⟩∘⟨refl) ⟩
distributeˡ⁻¹ ∘ [ ⟨ idC ∘ π₁ ∘ idC ∘ π₁ , distributeˡ⁻¹ ∘ ⟨ (π₂ ∘ π₁) ∘ (idC ⁂ i₁) , π₂ ∘ (idC ⁂ i₁) ⟩ ⟩ , ⟨ idC ∘ π₁ ∘ idC ∘ π₁ , distributeˡ⁻¹ ∘ ⟨ (π₂ ∘ π₁) ∘ (idC ⁂ i₂) , π₂ ∘ (idC ⁂ i₂) ⟩ ⟩ ] ∘ distributeˡ⁻¹ ≈⟨ sym (refl⟩∘⟨ []-cong₂ (⟨⟩-cong₂ (pullʳ (pullʳ π₁∘⁂)) (pullʳ ⟨⟩∘)) (⟨⟩-cong₂ (pullʳ (pullʳ π₁∘⁂)) (pullʳ ⟨⟩∘)) ⟩∘⟨refl) ⟩
distributeˡ⁻¹ ∘ [ ⟨ (idC ∘ π₁ ∘ π₁) ∘ (idC ⁂ i₁) , (distributeˡ⁻¹ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩) ∘ (idC ⁂ i₁) ⟩ , ⟨ (idC ∘ π₁ ∘ π₁) ∘ (idC ⁂ i₂) , (distributeˡ⁻¹ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩) ∘ (idC ⁂ i₂) ⟩ ] ∘ distributeˡ⁻¹ ≈⟨ sym (refl⟩∘⟨ []-cong₂ ⟨⟩∘ ⟨⟩∘ ⟩∘⟨refl) ⟩
distributeˡ⁻¹ ∘ [ (⟨ idC ∘ π₁ ∘ π₁ , distributeˡ⁻¹ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ∘ (idC ⁂ i₁)) , (⟨ idC ∘ π₁ ∘ π₁ , distributeˡ⁻¹ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ∘ (idC ⁂ i₂)) ] ∘ distributeˡ⁻¹ ≈˘⟨ pullʳ (pullˡ ∘[]) ⟩
(distributeˡ⁻¹ ∘ ⟨ idC ∘ π₁ ∘ π₁ , distributeˡ⁻¹ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ distributeˡ ∘ distributeˡ⁻¹ ≈⟨ sym (introʳ (IsIso.isoʳ isIsoˡ)) ⟩
distributeˡ⁻¹ ∘ ⟨ idC ∘ π₁ ∘ π₁ , distributeˡ⁻¹ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ≈⟨ sym (refl⟩∘⟨ ⁂∘⟨⟩) ⟩
distributeˡ⁻¹ ∘ (idC ⁂ distributeˡ⁻¹) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ∎)
strongMonad : StrongMonad monoidal
strongMonad = record { M = monad ; strength = strength }