diff --git a/src/Algebra/Search.lagda.md b/src/Algebra/Search.lagda.md index 313dbaa..0d019a3 100644 --- a/src/Algebra/Search.lagda.md +++ b/src/Algebra/Search.lagda.md @@ -43,4 +43,8 @@ module Algebra.Search {o ℓ e} (ambient : Ambient o ℓ e) where IsSearchAlgebra⇒Search-Algebra : ∀ {A} (α : F-Algebra-on functor A) → IsSearchAlgebra α → Search-Algebra IsSearchAlgebra⇒Search-Algebra {A} α is = record { A = A ; search-algebra-on = record { α = α ; identity₁ = identity₁ ; identity₂ = identity₂ } } where open IsSearchAlgebra is + + Search-Algebra-on⇒IsSearchAlgebra : ∀ {A} → (search : Search-Algebra-on A) → IsSearchAlgebra (Search-Algebra-on.α search) + Search-Algebra-on⇒IsSearchAlgebra {A} search = record { identity₁ = identity₁ ; identity₂ = identity₂ } + where open Search-Algebra-on search ``` \ No newline at end of file diff --git a/src/Category/Instance/AmbientCategory.lagda.md b/src/Category/Instance/AmbientCategory.lagda.md index c1f26ce..9a39709 100644 --- a/src/Category/Instance/AmbientCategory.lagda.md +++ b/src/Category/Instance/AmbientCategory.lagda.md @@ -10,7 +10,9 @@ open import Categories.Category.Cartesian using (Cartesian) open import Categories.Category.BinaryProducts using (BinaryProducts) open import Categories.Category.Cartesian.Bundle using (CartesianCategory) 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.Category.Cocartesian using (Cocartesian) open import Categories.Object.NaturalNumbers.Parametrized using (ParametrizedNNO) open import Categories.Object.Exponential using (Exponential) @@ -47,8 +49,10 @@ module Category.Instance.AmbientCategory where open Cartesian cartesian public monoidal : Monoidal C monoidal = CartesianMonoidal.monoidal cartesian - -- open Terminal terminal public - -- Don't open the terminal object, because we are interested in many different terminal objects stemming from multiple categories + + symmetric : Symmetric monoidal + symmetric = symm C cartesian + open BinaryProducts products renaming (η to ⁂-η; g-η to ⁂-g-η; unique to ⟨⟩-unique; unique′ to ⟨⟩-unique′) public open ParametrizedNNO ℕ public renaming (η to pnno-η) diff --git a/src/Monad/Commutative.agda b/src/Monad/Commutative.agda new file mode 100644 index 0000000..070b9e7 --- /dev/null +++ b/src/Monad/Commutative.agda @@ -0,0 +1,35 @@ +{-# OPTIONS --without-K --safe #-} + +-- Commutative Monad on a symmetric monoidal category +-- https://ncatlab.org/nlab/show/commutative+monad + +module Monad.Commutative where + +open import Level +open import Data.Product using (_,_) + +open import Categories.Category.Core +open import Categories.Category.Monoidal +open import Categories.Category.Monoidal.Symmetric +open import Categories.Monad +open import Categories.Monad.Strong + +private + variable + o ℓ e : Level + +record CommutativeMonad {C : Category o ℓ e} {V : Monoidal C} (S : Symmetric V) (T : StrongMonad V) : Set (o ⊔ ℓ ⊔ e) where + open Category C + open Symmetric S + open StrongMonad T + + + private + σ : ∀ {X Y} → X ⊗₀ M.F.₀ Y ⇒ M.F.₀ (X ⊗₀ Y) + σ {X} {Y} = strengthen.η (X , Y) + + τ : ∀ {X Y} → M.F.₀ X ⊗₀ Y ⇒ M.F.₀ (X ⊗₀ Y) + τ {X} {Y} = M.F.₁ (braiding.⇐.η (X , Y)) ∘ σ ∘ braiding.⇒.η (M.F.₀ X , Y) + + field + commutes : ∀ {X Y} → M.μ.η (X ⊗₀ Y) ∘ M.F.₁ τ ∘ σ ≈ M.μ.η (X ⊗₀ Y) ∘ M.F.₁ σ ∘ τ \ No newline at end of file diff --git a/src/Monad/Instance/Delay.lagda.md b/src/Monad/Instance/Delay.lagda.md index 00d0bc8..e008a78 100644 --- a/src/Monad/Instance/Delay.lagda.md +++ b/src/Monad/Instance/Delay.lagda.md @@ -14,6 +14,7 @@ open import Categories.Monad.Strong open import Categories.Category.Construction.F-Coalgebras open import Categories.NaturalTransformation open import Category.Instance.AmbientCategory using (Ambient) +open import Monad.Commutative ``` --> ```agda @@ -204,6 +205,35 @@ and second that `extend f` is the unique morphism satisfying the commutative dia [ g , idC ] ∘ i₁ ≈⟨ inject₁ ⟩ g ∎ + -- Lemma 39: ▷ ∘ f* ≈ (▷ ∘ f)* ≈ f* ∘ ▷ + + module _ {X Y} (f : X ⇒ D₀ Y) where + private + helper : out ∘ [ f , extend' (▷ ∘ f) ] ∘ out ≈ [ out ∘ f , i₂ ∘ [ f , extend' (▷ ∘ f) ] ∘ out ] ∘ out + helper = pullˡ ∘[] ○ (([]-cong₂ refl (extendlaw (▷ ∘ f) ○ ((([]-cong₂ (pullˡ laterlaw) refl) ⟩∘⟨refl) ○ sym (pullˡ ∘[])))) ⟩∘⟨refl) + helper₁ : [ f , extend' (▷ ∘ f) ] ∘ out ≈ extend' f + helper₁ = sym (extend'-unique f ([ f , extend' (▷ ∘ f) ] ∘ out) helper) + + ▷∘extendˡ : ▷ ∘ extend' f ≈ extend' (▷ ∘ f) + ▷∘extendˡ = sym (begin + extend' (▷ ∘ f) ≈⟨ introˡ (_≅_.isoˡ out-≅) ⟩ + (out⁻¹ ∘ out) ∘ extend' (▷ ∘ f) ≈⟨ pullʳ (extendlaw (▷ ∘ f)) ⟩ + out⁻¹ ∘ [ out ∘ ▷ ∘ f , i₂ ∘ extend' (▷ ∘ f) ] ∘ out ≈⟨ (refl⟩∘⟨ (([]-cong₂ (pullˡ laterlaw) refl) ○ (sym ∘[])) ⟩∘⟨refl) ⟩ + out⁻¹ ∘ (i₂ ∘ [ f , extend' (▷ ∘ f) ]) ∘ out ≈⟨ (refl⟩∘⟨ (pullʳ helper₁)) ⟩ + out⁻¹ ∘ i₂ ∘ extend' f ≈⟨ sym-assoc ⟩ + ▷ ∘ extend' f ∎) + + ▷∘extend-comm : ▷ ∘ extend' f ≈ extend' f ∘ ▷ + ▷∘extend-comm = sym (begin + extend' f ∘ ▷ ≈⟨ introˡ (_≅_.isoˡ out-≅) ⟩ + (out⁻¹ ∘ out) ∘ extend' f ∘ ▷ ≈⟨ pullʳ (pullˡ (extendlaw f)) ⟩ + out⁻¹ ∘ ([ out ∘ f , i₂ ∘ extend' f ] ∘ out) ∘ ▷ ≈⟨ (refl⟩∘⟨ pullʳ laterlaw) ⟩ + out⁻¹ ∘ [ out ∘ f , i₂ ∘ extend' f ] ∘ i₂ ≈⟨ (refl⟩∘⟨ inject₂) ○ sym-assoc ⟩ + ▷ ∘ extend' f ∎) + + ▷∘extendʳ : extend' f ∘ ▷ ≈ extend' (▷ ∘ f) + ▷∘extendʳ = (sym ▷∘extend-comm) ○ ▷∘extendˡ + kleisli : KleisliTriple C kleisli = record { F₀ = D₀ @@ -242,47 +272,47 @@ and second that `extend f` is the unique morphism satisfying the commutative dia identityʳ' : ∀ {X Y : Obj} {f : X ⇒ D₀ Y} → extend' f ∘ now {X} ≈ f identityʳ' {X} {Y} {f} = begin - extend' f ∘ now ≈⟨ insertˡ (_≅_.isoˡ out-≅) ⟩∘⟨refl ⟩ - (out⁻¹ ∘ out ∘ extend' f) ∘ now ≈⟨ (refl⟩∘⟨ (extendlaw f)) ⟩∘⟨refl ⟩ - (out⁻¹ ∘ [ out ∘ f , i₂ ∘ extend' f ] ∘ out) ∘ now ≈⟨ pullʳ (pullʳ unitlaw) ⟩ - out⁻¹ ∘ [ out ∘ f , i₂ ∘ extend' f ] ∘ i₁ ≈⟨ refl⟩∘⟨ inject₁ ⟩ + extend' f ∘ now ≈⟨ insertˡ (_≅_.isoˡ out-≅) ⟩∘⟨refl ⟩ + (out⁻¹ ∘ out ∘ extend' f) ∘ now ≈⟨ (refl⟩∘⟨ (extendlaw f)) ⟩∘⟨refl ⟩ + (out⁻¹ ∘ [ out ∘ f , i₂ ∘ extend' f ] ∘ out) ∘ now ≈⟨ pullʳ (pullʳ unitlaw) ⟩ + out⁻¹ ∘ [ out ∘ f , i₂ ∘ extend' f ] ∘ i₁ ≈⟨ refl⟩∘⟨ inject₁ ⟩ out⁻¹ ∘ out ∘ f ≈⟨ cancelˡ (_≅_.isoˡ out-≅) ⟩ - f ∎ + f ∎ identityˡ' : ∀ {X} → extend' now ≈ idC identityˡ' {X} = Terminal.⊤-id (coalgebras X) (record { f = extend' now ; commutes = begin out ∘ extend' now ≈⟨ pullˡ ((commutes (! (coalgebras X) {A = alg now}))) ⟩ - ((idC +₁ (u (! (coalgebras X) {A = alg now}))) ∘ α (alg now)) ∘ i₁ ≈⟨ pullʳ inject₁ ⟩ + ((idC +₁ (u (! (coalgebras X) {A = alg now}))) ∘ α (alg now)) ∘ i₁ ≈⟨ pullʳ inject₁ ⟩ (idC +₁ (u (! (coalgebras X) {A = alg now}))) - ∘ [ [ i₁ , i₂ ∘ i₂ ] ∘ (out ∘ now) , i₂ ∘ i₁ ] ∘ out ≈⟨ refl⟩∘⟨ []-cong₂ ((refl⟩∘⟨ unitlaw) ○ inject₁) refl ⟩∘⟨refl ⟩ + ∘ [ [ i₁ , i₂ ∘ i₂ ] ∘ (out ∘ now) , i₂ ∘ i₁ ] ∘ out ≈⟨ refl⟩∘⟨ []-cong₂ ((refl⟩∘⟨ unitlaw) ○ inject₁) refl ⟩∘⟨refl ⟩ (idC +₁ (u (! (coalgebras X) {A = alg now}))) ∘ [ i₁ , i₂ ∘ i₁ ] ∘ out ≈⟨ pullˡ ∘[] ⟩ [ (idC +₁ (u (! (coalgebras X) {A = alg now}))) ∘ i₁ , (idC +₁ (u (! (coalgebras X) {A = alg now}))) ∘ i₂ ∘ i₁ ] ∘ out ≈⟨ []-cong₂ +₁∘i₁ (pullˡ +₁∘i₂) ⟩∘⟨refl ⟩ [ i₁ ∘ idC , (i₂ ∘ (u (! (coalgebras X) {A = alg now}))) ∘ i₁ ] ∘ out ≈⟨ []-cong₂ refl assoc ⟩∘⟨refl ⟩ - [ i₁ ∘ idC , i₂ ∘ (extend' now) ] ∘ out ≈˘⟨ []∘+₁ ⟩∘⟨refl ⟩ - ([ i₁ , i₂ ] ∘ (idC +₁ extend' now)) ∘ out ≈⟨ elimˡ +-η ⟩∘⟨refl ⟩ - (idC +₁ extend' now) ∘ out ∎ }) + [ i₁ ∘ idC , i₂ ∘ (extend' now) ] ∘ out ≈˘⟨ []∘+₁ ⟩∘⟨refl ⟩ + ([ i₁ , i₂ ] ∘ (idC +₁ extend' now)) ∘ out ≈⟨ elimˡ +-η ⟩∘⟨refl ⟩ + (idC +₁ extend' now) ∘ out ∎ }) assoc' : ∀ {X Y Z : Obj} {g : X ⇒ D₀ Y} {h : Y ⇒ D₀ Z} → extend' (extend' h ∘ g) ≈ extend' h ∘ extend' g assoc' {X} {Y} {Z} {g} {h} = extend'-unique (extend' h ∘ g) (extend' h ∘ extend' g) (begin - out ∘ extend' h ∘ extend' g ≈⟨ pullˡ (extendlaw h) ⟩ - ([ out ∘ h , i₂ ∘ extend' h ] ∘ out) ∘ extend' g ≈⟨ pullʳ (extendlaw g) ⟩ + out ∘ extend' h ∘ extend' g ≈⟨ pullˡ (extendlaw h) ⟩ + ([ out ∘ h , i₂ ∘ extend' h ] ∘ out) ∘ extend' g ≈⟨ pullʳ (extendlaw g) ⟩ [ out ∘ h , i₂ ∘ extend' h ] ∘ [ out ∘ g , i₂ ∘ extend' g ] ∘ out ≈⟨ pullˡ ∘[] ⟩ [ [ out ∘ h , i₂ ∘ extend' h ] ∘ out ∘ g - , [ out ∘ h , i₂ ∘ extend' h ] ∘ i₂ ∘ extend' g ] ∘ out ≈⟨ []-cong₂ (pullˡ (⟺ (extendlaw h))) (pullˡ inject₂) ⟩∘⟨refl ⟩ - [ (out ∘ extend' h) ∘ g , (i₂ ∘ extend' h) ∘ extend' g ] ∘ out ≈⟨ ([]-cong₂ assoc assoc) ⟩∘⟨refl ⟩ - [ out ∘ extend' h ∘ g , i₂ ∘ extend' h ∘ extend' g ] ∘ out ∎) + , [ out ∘ h , i₂ ∘ extend' h ] ∘ i₂ ∘ extend' g ] ∘ out ≈⟨ []-cong₂ (pullˡ (⟺ (extendlaw h))) (pullˡ inject₂) ⟩∘⟨refl ⟩ + [ (out ∘ extend' h) ∘ g , (i₂ ∘ extend' h) ∘ extend' g ] ∘ out ≈⟨ ([]-cong₂ assoc assoc) ⟩∘⟨refl ⟩ + [ out ∘ extend' h ∘ g , i₂ ∘ extend' h ∘ extend' g ] ∘ out ∎) extend-≈' : ∀ {X} {Y} {f g : X ⇒ D₀ Y} → f ≈ g → extend' f ≈ extend' g extend-≈' {X} {Y} {f} {g} eq = begin u (! (coalgebras Y) {A = alg f }) ∘ i₁ {B = D₀ Y} ≈⟨ (!-unique (coalgebras Y) (record { f = (u (! (coalgebras Y) {A = alg g }) ∘ idC) ; commutes = begin α (⊤ (coalgebras Y)) ∘ u (! (coalgebras Y)) ∘ idC ≈⟨ refl⟩∘⟨ identityʳ ⟩ α (⊤ (coalgebras Y)) ∘ u (! (coalgebras Y)) ≈⟨ commutes (! (coalgebras Y)) ⟩ - (idC +₁ u (! (coalgebras Y))) ∘ α (alg g) ≈˘⟨ Functor.F-resp-≈ (Y +-) identityʳ ⟩∘⟨ αf≈αg eq ⟩ - (idC +₁ u (! (coalgebras Y)) ∘ idC) ∘ α (alg f) ∎ })) + (idC +₁ u (! (coalgebras Y))) ∘ α (alg g) ≈˘⟨ Functor.F-resp-≈ (Y +-) identityʳ ⟩∘⟨ αf≈αg eq ⟩ + (idC +₁ u (! (coalgebras Y)) ∘ idC) ∘ α (alg f) ∎ })) ⟩∘⟨refl ⟩ (u (! (coalgebras Y) {A = alg g }) ∘ idC) ∘ i₁ {B = D₀ Y} ≈⟨ identityʳ ⟩∘⟨refl ⟩ - extend' g ∎ + extend' g ∎ monad : Monad C monad = Kleisli⇒Monad C kleisli @@ -291,270 +321,3 @@ and second that `extend f` is the unique morphism satisfying the commutative dia functor : Endofunctor C functor = Monad.F monad ``` - -Next we will show that the delay monad is strong, by giving a natural transformation `strengthen : X × DY ⇒ D (X × Y) - -```agda - module _ where - open Functor - open import Categories.Category.Monoidal.Core - open Monoidal monoidal - open import Categories.Monad.Relative using () renaming (Monad to RMonad) - open RMonad kleisli using (extend; extend-≈) renaming (assoc to k-assoc; identityʳ to k-identityʳ) - open import Categories.Category.Product renaming (Product to CProduct; _⁂_ to _×C_) - open Monad monad using () renaming (η to η'; μ to μ') - module η = NaturalTransformation η' - module μ = NaturalTransformation μ' - strength : Strength monoidal monad - strength = record - { strengthen = ntHelper (record - { η = τ - ; commute = commute' }) - ; identityˡ = identityˡ' -- triangle - ; η-comm = begin -- η-τ - τ _ ∘ (idC ⁂ now) ≈⟨ refl⟩∘⟨ (⁂-cong₂ (sym identity²) refl ○ sym ⁂∘⁂) ⟩ - τ _ ∘ (idC ⁂ out⁻¹) ∘ (idC ⁂ i₁) ≈⟨ pullˡ (τ-helper _) ⟩ - (out⁻¹ ∘ (idC +₁ τ _) ∘ distributeˡ⁻¹) ∘ (idC ⁂ i₁) ≈⟨ pullʳ (pullʳ dstr-law₁) ⟩ - out⁻¹ ∘ (idC +₁ τ _) ∘ i₁ ≈⟨ refl⟩∘⟨ +₁∘i₁ ⟩ - out⁻¹ ∘ i₁ ∘ idC ≈⟨ refl⟩∘⟨ identityʳ ⟩ - now ∎ - ; μ-η-comm = μ-η-comm' -- μ-τ - ; strength-assoc = strength-assoc' -- square - } - where - open import Agda.Builtin.Sigma - out-law : ∀ {X Y} (f : X ⇒ Y) → out {Y} ∘ extend (now ∘ f) ≈ (f +₁ extend (now ∘ f)) ∘ out {X} - out-law {X} {Y} f = begin - out ∘ extend (now ∘ f) ≈⟨ extendlaw (now ∘ f) ⟩ - [ out ∘ now ∘ f , i₂ ∘ extend (now ∘ f) ] ∘ out ≈⟨ ([]-cong₂ (pullˡ unitlaw) refl) ⟩∘⟨refl ⟩ - (f +₁ extend (now ∘ f)) ∘ out ∎ - 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₂ - dstr-law₂ = (refl⟩∘⟨ (sym inject₂)) ○ (cancelˡ (IsIso.isoˡ isIsoˡ)) - - module _ (P : Category.Obj (CProduct C C)) where - X = fst P - Y = snd 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ʳ dstr-law₁) ⟩ - out⁻¹ ∘ (idC +₁ τ) ∘ i₁ ≈⟨ refl⟩∘⟨ +₁∘i₁ ⟩ - out⁻¹ ∘ i₁ ∘ idC ≈⟨ refl⟩∘⟨ identityʳ ⟩ - now ∎ - - τ-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 })) - - identityˡ' : ∀ {X : Obj} → extend (now ∘ π₂) ∘ τ (Terminal.⊤ terminal , X) ≈ π₂ - identityˡ' {X} = begin - extend (now ∘ π₂) ∘ τ _ ≈⟨ sym (Terminal.!-unique (coalgebras X) {A = record { A = Terminal.⊤ terminal × D₀ X ; α = (π₂ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) }} (record { f = extend (now ∘ π₂) ∘ τ _ ; commutes = begin - out ∘ extend (now ∘ π₂) ∘ τ _ ≈⟨ refl⟩∘⟨ (refl⟩∘⟨ (sym identityʳ)) ⟩ - out ∘ extend (now ∘ π₂) ∘ τ _ ∘ idC ≈⟨ pullˡ diag₃ ⟩ - ((π₂ +₁ extend (now ∘ π₂)) ∘ out) ∘ τ _ ∘ idC ≈⟨ pullʳ (pullˡ (diag₂ (Terminal.⊤ terminal , X))) ⟩ - (π₂ +₁ extend (now ∘ π₂)) ∘ ((idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out)) ∘ idC ≈⟨ refl⟩∘⟨ (pullʳ (assoc ○ sym diag₁)) ⟩ - (π₂ +₁ extend (now ∘ π₂)) ∘ (idC +₁ τ _) ∘ (⟨ Terminal.! terminal , idC ⟩ +₁ idC) ∘ (π₂ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (pullˡ (+₁∘+₁ ○ +₁-cong₂ (_≅_.isoˡ ⊤×A≅A) identity² ○ CC.+-unique ((identity² ⟩∘⟨refl) ○ id-comm-sym) ((identity² ⟩∘⟨refl) ○ id-comm-sym)) ) ⟩ - (π₂ +₁ extend (now ∘ π₂)) ∘ (idC +₁ τ _) ∘ (idC ∘ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ pullˡ +₁∘+₁ ⟩ - (π₂ ∘ idC +₁ extend (now ∘ π₂) ∘ τ _) ∘ (idC ∘ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ (+₁-cong₂ id-comm refl) ⟩∘⟨refl ⟩ - (idC ∘ π₂ +₁ extend (now ∘ π₂) ∘ τ _) ∘ (idC ∘ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈˘⟨ pullˡ +₁∘+₁ ⟩ - (idC +₁ extend (now ∘ π₂)) ∘ (π₂ +₁ τ _) ∘ (idC ∘ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ refl⟩∘⟨ (refl⟩∘⟨ (elimˡ identity²)) ⟩ - (idC +₁ extend (now ∘ π₂)) ∘ (π₂ +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈˘⟨ refl⟩∘⟨ ((+₁-cong₂ identityˡ identityʳ) ⟩∘⟨refl) ⟩ - (idC +₁ extend (now ∘ π₂)) ∘ (idC ∘ π₂ +₁ τ _ ∘ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈˘⟨ pullʳ (pullˡ +₁∘+₁) ⟩ - ((idC +₁ extend (now ∘ π₂)) ∘ (idC +₁ τ _)) ∘ (π₂ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈˘⟨ (homomorphism (X +-)) ⟩∘⟨refl ⟩ - (idC +₁ extend (now ∘ π₂) ∘ τ _) ∘ (π₂ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ∎ })) ⟩ - u (Terminal.! (coalgebras X)) ≈⟨ Terminal.!-unique (coalgebras X) {A = record { A = Terminal.⊤ terminal × D₀ X ; α = (π₂ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) }} (record { f = π₂ ; commutes = begin - out ∘ π₂ ≈˘⟨ π₂∘⁂ ⟩ - π₂ ∘ (idC ⁂ out) ≈˘⟨ pullˡ distribute₂ ⟩ -- TODO this might be wrong if distribute₂ is unprovable - (π₂ +₁ π₂) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈˘⟨ (+₁-cong₂ identityˡ identityʳ) ⟩∘⟨refl ⟩ - (idC ∘ π₂ +₁ π₂ ∘ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈˘⟨ pullˡ +₁∘+₁ ⟩ - (idC +₁ π₂) ∘ (π₂ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ∎ }) ⟩ - π₂ ∎ - where - diag₁ : (⟨ Terminal.! terminal , idC ⟩ +₁ idC) ∘ (π₂ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈ distributeˡ⁻¹ {Terminal.⊤ terminal} {X} {D₀ X} ∘ (idC ⁂ out) ∘ idC - diag₁ = 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ˡ (CC.+-unique id-comm-sym id-comm-sym) ⟩ - distributeˡ⁻¹ ∘ (idC ⁂ out) ∘ idC ∎ - diag₂ = τ-law - diag₃ : out {X} ∘ extend (now ∘ π₂ {A = Terminal.⊤ terminal} {B = X}) ≈ (π₂ +₁ extend (now ∘ π₂)) ∘ out - diag₃ = out-law π₂ - distribute₂ : ∀ {A B C} → (π₂ +₁ π₂) ∘ distributeˡ⁻¹ {A} {B} {C} ≈ π₂ - distribute₂ = sym (begin - π₂ ≈⟨ introʳ (IsIso.isoʳ isIsoˡ) ⟩ - π₂ ∘ distributeˡ ∘ distributeˡ⁻¹ ≈⟨ pullˡ ∘[] ⟩ - [ π₂ ∘ ((idC ⁂ i₁)) , π₂ ∘ (idC ⁂ i₂) ] ∘ distributeˡ⁻¹ ≈⟨ ([]-cong₂ π₂∘⁂ π₂∘⁂) ⟩∘⟨refl ⟩ - (π₂ +₁ π₂) ∘ distributeˡ⁻¹ ∎) - - μ-η-comm' : ∀ {X Y} → extend idC ∘ (extend (now ∘ τ _)) ∘ τ _ ≈ τ (X , Y) ∘ (idC ⁂ extend idC) - μ-η-comm' {X} {Y} = begin - extend idC ∘ (extend (now ∘ τ _)) ∘ τ _ ≈⟨ sym (Terminal.!-unique (coalgebras (X × Y)) (record { f = extend idC ∘ (extend (now ∘ τ _)) ∘ τ _ ; commutes = begin - out ∘ extend idC ∘ extend (now ∘ τ (X , Y)) ∘ τ _ ≈⟨ refl⟩∘⟨ (pullˡ id*∘Dτ) ⟩ - out ∘ extend (τ (X , Y)) ∘ τ _ ≈⟨ square ⟩ - [ out ∘ τ _ , i₂ ∘ extend (τ _) ] ∘ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ sym-assoc ○ sym-assoc ○ (assoc ○ tri) ⟩∘⟨refl ⟩ - ((idC +₁ extend (τ _) ∘ τ _) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹) ∘ (idC ⁂ out) ≈⟨ assoc ○ refl⟩∘⟨ assoc ⟩ - (idC +₁ (extend (τ _) ∘ τ _)) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ (+₁-cong₂ refl (sym (pullˡ id*∘Dτ))) ⟩∘⟨refl ⟩ - (idC +₁ (extend idC ∘ extend (now ∘ τ (X , Y)) ∘ τ _)) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ∎ })) ⟩ - u (Terminal.! (coalgebras (X × Y)) {A = record { A = X × D₀ (D₀ Y) ; α = [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) }}) ≈⟨ Terminal.!-unique (coalgebras (X × Y)) (record { f = τ _ ∘ (idC ⁂ extend idC) ; commutes = begin - out ∘ τ _ ∘ (idC ⁂ extend idC) ≈⟨ pullˡ (τ-law (X , Y)) ⟩ - ((idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out)) ∘ (idC ⁂ extend idC) ≈⟨ pullʳ (pullʳ (⁂∘⁂ ○ ⁂-cong₂ identity² refl)) ⟩ - (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out ∘ extend idC) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⁂-cong₂ refl (extendlaw idC) ⟩ - (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ [ out ∘ idC , i₂ ∘ extend idC ] ∘ out) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⁂-cong₂ refl (([]-cong₂ identityʳ refl) ⟩∘⟨refl) ⟩ - (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ [ out , i₂ ∘ extend idC ] ∘ out) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ sym (⁂∘⁂ ○ ⁂-cong₂ identity² refl) ⟩ - (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ [ out , i₂ ∘ extend idC ]) ∘ (idC ⁂ out) ≈⟨ sym-assoc ○ pullˡ (assoc ○ tri₂) ⟩ - ((idC +₁ τ _ ∘ (idC ⁂ extend idC)) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹) ∘ (idC ⁂ out) ≈⟨ assoc ○ refl⟩∘⟨ assoc ⟩ - (idC +₁ τ _ ∘ (idC ⁂ extend idC)) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ∎ }) ⟩ - τ _ ∘ (idC ⁂ extend idC) ∎ - where - -- diagram: https://q.uiver.app/#q=WzAsNyxbMCwwLCJYXFx0aW1lcyBERFkiXSxbMiwwLCJEKFhcXHRpbWVzIERZKSJdLFs0LDAsIkREKFhcXHRpbWVzIFkpIl0sWzAsMiwiWFxcdGltZXMgKERZK0REWSkiXSxbMiwyLCJYXFx0aW1lcyBEWSsgWFxcdGltZXMgRERZIl0sWzQsMiwiWFxcdGltZXMgWSsgREQoWFxcdGltZXMgWSkiXSxbMCw0LCJYXFx0aW1lcyBZKyBYXFx0aW1lcyBERFkiXSxbMCwzLCJpZFxcdGltZXMgb3V0IiwyXSxbMCwxLCJcXHRhdSJdLFsxLDIsIlxcdGF1XioiXSxbMyw0LCIoaWQrXFx0YXUpZGlzdCJdLFs0LDUsIltvdXRcXHRhdSxpbnJcXHRhdV4qXSJdLFsyLDUsIm91dCJdLFsxLDRdLFs2LDUsImlkK1xcdGF1XipcXHRhdSIsMl0sWzMsNiwiWyhpZCArIGlkXFx0aW1lcyBub3cpZGlzdCAoaWRcXHRpbWVzIG91dCksaW5yXWRpc3QiLDJdXQ== - square : out ∘ extend (τ (X , Y)) ∘ τ _ ≈ [ out ∘ τ _ , i₂ ∘ extend (τ _) ] ∘ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) - square = begin - out ∘ extend (τ (X , Y)) ∘ τ _ ≈⟨ pullˡ (extendlaw (τ (X , Y))) ⟩ - ([ out ∘ τ (X , Y) , i₂ ∘ extend (τ (X , Y)) ] ∘ out) ∘ τ _ ≈⟨ pullʳ (τ-law _) ⟩ - [ out ∘ τ _ , i₂ ∘ extend (τ _) ] ∘ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ∎ - tri : [ out ∘ τ _ , i₂ ∘ extend (τ (X , Y)) ] ∘ (idC +₁ τ _) ∘ distributeˡ⁻¹ ≈ (idC +₁ extend (τ _) ∘ τ _) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹ - tri = begin - [ out ∘ τ _ , i₂ ∘ extend (τ (X , Y)) ] ∘ (idC +₁ τ _) ∘ distributeˡ⁻¹ ≈⟨ pullˡ []∘+₁ ⟩ - [ (out ∘ τ _) ∘ idC , (i₂ ∘ extend (τ (X , Y))) ∘ τ _ ] ∘ distributeˡ⁻¹ ≈⟨ ([]-cong₂ (identityʳ ○ τ-law (X , Y)) assoc) ⟩∘⟨refl ⟩ - [ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ∘ extend (τ (X , Y)) ∘ τ _ ] ∘ distributeˡ⁻¹ ≈⟨ sym (([]-cong₂ ((+₁-cong₂ refl k-identityʳ) ⟩∘⟨refl) refl) ⟩∘⟨refl) ⟩ - [ (idC +₁ extend (τ _) ∘ now) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ∘ extend (τ _) ∘ τ _ ] ∘ distributeˡ⁻¹ ≈⟨ sym (([]-cong₂ ((+₁-cong₂ identity² (pullʳ (τ-now (X , D₀ Y)))) ⟩∘⟨refl) refl) ⟩∘⟨refl) ⟩ - [ (idC ∘ idC +₁ (extend (τ _) ∘ τ _) ∘ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ∘ extend (τ _) ∘ τ _ ] ∘ distributeˡ⁻¹ ≈⟨ sym (([]-cong₂ (pullˡ +₁∘+₁) +₁∘i₂) ⟩∘⟨refl) ⟩ - [ (idC +₁ extend (τ _) ∘ τ _) ∘ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , (idC +₁ extend (τ _) ∘ τ _) ∘ i₂ ] ∘ distributeˡ⁻¹ ≈⟨ sym (pullˡ ∘[]) ⟩ - (idC +₁ extend (τ _) ∘ τ _) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹ ∎ - id*∘Dτ : extend idC ∘ extend (now ∘ τ _) ≈ extend (τ _) - id*∘Dτ = begin - extend idC ∘ extend (now ∘ τ _) ≈⟨ sym k-assoc ⟩ - extend (extend idC ∘ now ∘ τ _) ≈⟨ extend-≈ (pullˡ k-identityʳ) ⟩ - extend (idC ∘ τ _) ≈⟨ extend-≈ identityˡ ⟩ - extend (τ _) ∎ - tri₂' : (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ [ out , i₂ ∘ extend idC ]) ∘ [ (idC ⁂ i₁) , (idC ⁂ i₂) ] ≈ (idC +₁ τ _ ∘ (idC ⁂ extend idC)) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹ ∘ distributeˡ - tri₂' = begin - (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ [ out , i₂ ∘ extend idC ]) ∘ [ (idC ⁂ i₁) , (idC ⁂ i₂) ] ≈⟨ refl⟩∘⟨ (refl⟩∘⟨ ∘[]) ⟩ - (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ [ (idC ⁂ [ out , i₂ ∘ extend idC ]) ∘ (idC ⁂ i₁) , (idC ⁂ [ out , i₂ ∘ extend idC ]) ∘ (idC ⁂ i₂) ] ≈⟨ refl⟩∘⟨ refl⟩∘⟨ []-cong₂ ⁂∘⁂ ⁂∘⁂ ⟩ - (idC +₁ τ _) ∘ 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 +₁ τ _) ∘ distributeˡ⁻¹ ∘ [ idC ⁂ out , idC ⁂ i₂ ∘ extend idC ] ≈⟨ refl⟩∘⟨ ∘[] ⟩ - (idC +₁ τ _) ∘ [ distributeˡ⁻¹ ∘ (idC ⁂ out) , distributeˡ⁻¹ ∘ (idC ⁂ i₂ ∘ extend idC) ] ≈⟨ ∘[] ⟩ - [ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ i₂ ∘ extend idC) ] ≈⟨ sym ([]-cong₂ refl (pullʳ (pullʳ (⁂∘⁂ ○ ⁂-cong₂ identity² refl)))) ⟩ - [ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , ((idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ i₂)) ∘ (idC ⁂ extend idC) ] ≈⟨ []-cong₂ refl ((refl⟩∘⟨ dstr-law₂) ⟩∘⟨refl) ⟩ - [ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , ((idC +₁ τ _) ∘ i₂) ∘ (idC ⁂ extend idC) ] ≈⟨ []-cong₂ refl (pushˡ +₁∘i₂) ⟩ - [ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ∘ τ _ ∘ (idC ⁂ extend idC) ] ≈⟨ []-cong₂ ((+₁-cong₂ refl (introʳ (⟨⟩-unique id-comm (id-comm ○ (sym k-identityʳ) ⟩∘⟨refl)))) ⟩∘⟨refl) refl ⟩ - [ (idC +₁ τ _ ∘ (idC ⁂ extend idC ∘ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ∘ τ _ ∘ (idC ⁂ extend idC) ] ≈⟨ []-cong₂ ((sym (+₁-cong₂ refl (refl⟩∘⟨ (⁂∘⁂ ○ ⁂-cong₂ identity² refl)))) ⟩∘⟨refl) refl ⟩ - [ (idC +₁ τ _ ∘ (idC ⁂ extend idC) ∘ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ∘ τ _ ∘ (idC ⁂ extend idC) ] ≈⟨ sym ([]-cong₂ (pullˡ (+₁∘+₁ ○ +₁-cong₂ identity² assoc)) +₁∘i₂) ⟩ - [ (idC +₁ τ _ ∘ (idC ⁂ extend idC)) ∘ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , (idC +₁ τ _ ∘ (idC ⁂ extend idC)) ∘ i₂ ] ≈⟨ sym ∘[] ⟩ - (idC +₁ τ _ ∘ (idC ⁂ extend idC)) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ≈⟨ sym (refl⟩∘⟨ (elimʳ (IsIso.isoˡ isIsoˡ))) ⟩ - (idC +₁ τ _ ∘ (idC ⁂ extend idC)) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹ ∘ distributeˡ ∎ - tri₂ : (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ [ out , i₂ ∘ extend idC ]) ≈ (idC +₁ τ _ ∘ (idC ⁂ extend idC)) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹ - tri₂ = iso-epi-from - (record { from = distributeˡ ; to = distributeˡ⁻¹ ; iso = IsIso.iso isIsoˡ }) - ((idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ [ out , i₂ ∘ extend idC ])) - ((idC +₁ τ _ ∘ (idC ⁂ extend idC)) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹) - (assoc ○ refl⟩∘⟨ assoc ○ tri₂' ○ sym-assoc ○ sym-assoc ○ assoc ⟩∘⟨refl) - - strength-assoc' : ∀ {X Y Z} → extend (now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ τ ((X × Y), Z) ≈ τ _ ∘ (idC ⁂ τ _) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ - strength-assoc' {X} {Y} {Z} = begin - extend (now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ τ _ ≈⟨ sym (Terminal.!-unique (coalgebras (X × Y × Z)) (record { f = extend (now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ τ _ ; commutes = begin - out ∘ extend (now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ τ _ ≈⟨ pullˡ (extendlaw (now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩)) ⟩ - ([ out ∘ now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ , i₂ ∘ extend (now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ] ∘ out) ∘ τ _ ≈⟨ pullʳ (τ-law (X × Y , Z)) ⟩ - [ out ∘ now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ , i₂ ∘ extend (now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ] ∘ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ ([]-cong₂ (pullˡ unitlaw) refl) ⟩∘⟨refl ⟩ - (⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ +₁ extend (now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩)) ∘ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ pullˡ +₁∘+₁ ⟩ - (⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ∘ idC +₁ extend (now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ (+₁-cong₂ id-comm (sym identityʳ)) ⟩∘⟨refl ⟩ - (idC ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ +₁ (extend (now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ τ _) ∘ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ sym (pullˡ +₁∘+₁) ⟩ - (idC +₁ extend (now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ τ _) ∘ (⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ∎ })) ⟩ - u (Terminal.! (coalgebras (X × Y × Z)) {A = record { A = (X × Y) × D₀ Z ; α = (⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) }}) ≈⟨ Terminal.!-unique (coalgebras (X × Y × Z)) (record { f = τ _ ∘ (idC ⁂ τ _) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ; commutes = begin - out ∘ τ _ ∘ (idC ⁂ τ _) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ≈⟨ pullˡ (τ-law (X , Y × Z)) ⟩ - ((idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out)) ∘ (idC ⁂ τ _) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ≈⟨ pullʳ (pullˡ (pullʳ ⁂∘⁂)) ⟩ - (idC +₁ τ _) ∘ (distributeˡ⁻¹ ∘ (idC ∘ idC ⁂ out ∘ τ _)) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ≈⟨ refl⟩∘⟨ assoc ⟩ - (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ∘ idC ⁂ out ∘ τ _) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ≈˘⟨ refl⟩∘⟨ (refl⟩∘⟨ (⁂-cong₂ identityʳ (assoc ○ sym (τ-law (Y , Z)))) ⟩∘⟨refl) ⟩ - (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ ((idC ∘ idC) ∘ idC ⁂ ((idC +₁ τ _) ∘ distributeˡ⁻¹) ∘ (idC ⁂ out)) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ≈⟨ sym (refl⟩∘⟨ (pullʳ (pullˡ ⁂∘⁂ ○ pullˡ ⁂∘⁂))) ⟩ - (idC +₁ τ _) ∘ (distributeˡ⁻¹ ∘ (idC ⁂ (idC +₁ τ _))) ∘ (idC ⁂ distributeˡ⁻¹) ∘ (idC ⁂ (idC ⁂ out)) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ≈⟨ refl⟩∘⟨ (refl⟩∘⟨ (refl⟩∘⟨ helper₁)) ⟩ - (idC +₁ τ _) ∘ (distributeˡ⁻¹ ∘ (idC ⁂ (idC +₁ τ _))) ∘ (idC ⁂ distributeˡ⁻¹) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ∘ (idC ⁂ out) ≈⟨ refl⟩∘⟨ (helper₂ ⟩∘⟨refl) ⟩ - (idC +₁ τ _) ∘ ((idC +₁ (idC ⁂ τ (Y , Z))) ∘ distributeˡ⁻¹) ∘ (idC ⁂ distributeˡ⁻¹) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ∘ (idC ⁂ out) ≈⟨ refl⟩∘⟨ (assoc ○ refl⟩∘⟨ sym assoc²') ⟩ - (idC +₁ τ _) ∘ (idC +₁ (idC ⁂ τ (Y , Z))) ∘ (distributeˡ⁻¹ ∘ (idC ⁂ distributeˡ⁻¹) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ (idC ⁂ out) ≈⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ identity² refl) ⟩ - (idC +₁ τ _ ∘ (idC ⁂ τ (Y , Z))) ∘ (distributeˡ⁻¹ ∘ (idC ⁂ distributeˡ⁻¹) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ (idC ⁂ out) ≈⟨ refl⟩∘⟨ (helper₃ ⟩∘⟨refl) ⟩ - (idC +₁ τ _ ∘ (idC ⁂ τ (Y , Z))) ∘ ((⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ +₁ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ distributeˡ⁻¹) ∘ (idC ⁂ out) ≈⟨ assoc²'' ⟩ - ((idC +₁ τ _ ∘ (idC ⁂ τ _)) ∘ (⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ +₁ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ sym ((+₁-cong₂ refl (identityʳ ○ sym-assoc) ○ sym +₁∘+₁) ⟩∘⟨refl) ⟩ - (idC ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ +₁ (τ _ ∘ (idC ⁂ τ _) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ sym (pullˡ +₁∘+₁) ⟩ - (idC +₁ τ _ ∘ (idC ⁂ τ _) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ (⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ∎ }) ⟩ - τ _ ∘ (idC ⁂ τ _) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ∎ - 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 +₁ τ _)) ≈ (idC +₁ (idC ⁂ τ (Y , Z))) ∘ distributeˡ⁻¹ - helper₂ = sym (distribute₁ idC idC (τ _)) ○ (+₁-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 dstr-law₁))) (⟨⟩-cong₂ identityˡ ((pushˡ (sym dstr-law₂)))) ⟩∘⟨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ˡ⁻¹) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ∎) --- {- ⁂ ⊤ ○ --- Diagram for identityˡ': --- https://q.uiver.app/#q=WzAsOSxbMCwyLCIxIFxcdGltZXMgREIiXSxbMiwyLCIxIFxcdGltZXMgKEIgKyBEQikiXSxbNiwyLCIxIFxcdGltZXMgQiArIDEgXFx0aW1lcyBEQiJdLFswLDQsIkQoMSBcXHRpbWVzIEIpIl0sWzYsNCwiKDEgXFx0aW1lcyBCKSArIEQoMSBcXHRpbWVzIEIpIl0sWzAsNiwiREIiXSxbNiw2LCJCICsgREIiXSxbMCwwLCIxIFxcdGltZXMgREIiXSxbNiwwLCJCICsgMSBcXHRpbWVzIERCIl0sWzAsMSwiaWQgXFx0aW1lcyBvdXQiXSxbMSwyLCJkaXN0cmliXnstMX0iXSxbMCwzLCJcXHRhdSIsMl0sWzUsNiwib3V0IiwyXSxbMyw0LCJvdXQiLDJdLFsyLDQsImlkICsgXFx0YXUiXSxbMyw1LCJEIFxccGlfMiJdLFs0LDYsIlxccGlfMiArIEQgXFxwaV8yIl0sWzcsOCwiKFxccGlfMiArIGlkKSBcXGNpcmMgZGlzdHJpYl57LTF9IFxcY2lyYyAoaWQgXFx0aW1lcyBvdXQpIl0sWzcsMCwiaWQiXSxbOCwyLCJcXGxhbmdsZSAhICwgaWQgXFxyYW5nbGUgKyBpZCJdXQ== --- -} - commute' : ∀ {P₁ : Category.Obj (CProduct C C)} {P₂ : Category.Obj (CProduct C C)} (fg : _[_,_] (CProduct C C) P₁ P₂) - → τ P₂ ∘ ((fst fg) ⁂ extend (now ∘ (snd fg))) ≈ extend (now ∘ ((fst fg) ⁂ (snd fg))) ∘ τ P₁ - commute' {(U , V)} {(W , X)} (f , g) = begin - τ _ ∘ (f ⁂ extend (now ∘ g)) ≈⟨ sym (!-unique (record { f = τ _ ∘ (f ⁂ extend (now ∘ g)) ; commutes = 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₁ 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) ∎ })) ⟩ - u ! ≈⟨ !-unique (record { f = extend (now ∘ (f ⁂ g)) ∘ τ _ ; commutes = begin - out ∘ extend (now ∘ (f ⁂ g)) ∘ τ _ ≈⟨ 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 +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ sym-assoc ○ sym-assoc ⟩ - ((((f ⁂ g) +₁ (extend (now ∘ (f ⁂ g)))) ∘ (idC +₁ τ _)) ∘ 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) ∎ }) ⟩ - extend (now ∘ (f ⁂ g)) ∘ τ _ ∎ - where - open Terminal (coalgebras (W × X)) - alg' : F-Coalgebra ((W × X) +-) - alg' = record { A = U × D₀ V ; α = ((f ⁂ g) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) } - - strongMonad : StrongMonad monoidal - strongMonad = record { M = monad ; strength = strength } -``` diff --git a/src/Monad/Instance/Delay/Commutative.lagda.md b/src/Monad/Instance/Delay/Commutative.lagda.md new file mode 100644 index 0000000..91778d2 --- /dev/null +++ b/src/Monad/Instance/Delay/Commutative.lagda.md @@ -0,0 +1,32 @@ + + +```agda +module Monad.Instance.Delay.Commutative {o ℓ e} (ambient : Ambient o ℓ e) (D : DelayM ambient) where + open Ambient ambient + open DelayM D + open import Monad.Instance.Delay.Strong ambient D + open Functor + open Monoidal monoidal + open RMonad kleisli using (extend; extend-≈) renaming (assoc to k-assoc; identityʳ to k-identityʳ) + open Monad monad using (η; μ) +``` + +# The Delay Monad is commutative + +```agda + commutativeMonad : CommutativeMonad symmetric strongMonad + commutativeMonad = record { commutes = {! !} } +``` \ No newline at end of file diff --git a/src/Monad/Instance/Delay/Properties.lagda.md b/src/Monad/Instance/Delay/Properties.lagda.md index 2ea1c8c..ae73338 100644 --- a/src/Monad/Instance/Delay/Properties.lagda.md +++ b/src/Monad/Instance/Delay/Properties.lagda.md @@ -36,7 +36,7 @@ module Monad.Instance.Delay.Properties {o ℓ e} (ambient : Ambient o ℓ e) whe open Functor D-Functor using () renaming (F₁ to D₁; homomorphism to D-homomorphism; F-resp-≈ to D-resp-≈; identity to D-identity) open RMonad D-Kleisli using (extend; extend-≈) renaming (assoc to k-assoc; identityʳ to k-identityʳ; identityˡ to k-identityˡ) - open Monad D-Monad using () renaming (assoc to M-assoc; identityʳ to M-identityʳ) + open Monad D-Monad using (μ; η) renaming (assoc to M-assoc; identityʳ to M-identityʳ) open HomReasoning open M C open MR C @@ -80,15 +80,42 @@ module Monad.Instance.Delay.Properties {o ℓ e} (ambient : Ambient o ℓ e) whe 2⇒3 : cond-2 → cond-3 2⇒3 c-2 X = record - { elgot = {! !} + { elgot = Elgot-Algebra.algebra (D-Algebra+Search⇒Elgot D (record + { A = Ď₀ X + ; action = α + ; commute = epi-DDρ (α ∘ D₁ α) (α ∘ extend (idC)) (sym (begin + (α ∘ μ.η (Ď₀ X)) ∘ D₁ (D₁ ρ) ≈⟨ pullʳ (μ.commute ρ) ⟩ + α ∘ D₁ ρ ∘ μ.η (D₀ X) ≈⟨ pullˡ (sym ρ-algebra-morphism) ⟩ + (ρ ∘ μ.η X) ∘ μ.η (D₀ X) ≈⟨ pullʳ μ∘Dμ ⟩ + ρ ∘ μ.η X ∘ D₁ (μ.η X) ≈⟨ pullˡ ρ-algebra-morphism ⟩ + (α ∘ D₁ ρ) ∘ D₁ (μ.η X) ≈⟨ pullʳ (sym D-homomorphism) ⟩ + α ∘ D₁ (ρ ∘ μ.η X) ≈⟨ (refl⟩∘⟨ (D-resp-≈ ρ-algebra-morphism)) ⟩ + α ∘ D₁ (α ∘ D₁ ρ) ≈⟨ (refl⟩∘⟨ D-homomorphism) ⟩ + α ∘ D₁ α ∘ D₁ (D₁ ρ) ≈⟨ sym-assoc ⟩ + (α ∘ D₁ α) ∘ D₁ (D₁ ρ) ∎)) + ; identity = identity₁ + }) (Search-Algebra-on⇒IsSearchAlgebra D s-alg-on)) ; isFO = {! !} ; isStable = {! !} ; ρ-algebra-morphism = {! !} ; ρ-law = {! !} } + where + open cond-2' (c-2 X) + open Search-Algebra-on s-alg-on + epi-DDρ : Epi (D₁ (D₁ ρ)) + epi-DDρ = {! !} + μ∘Dμ : ∀ {X} → μ.η X ∘ μ.η (D₀ X) ≈ μ.η X ∘ D₁ (μ.η X) + μ∘Dμ {X} = begin + μ.η X ∘ μ.η (D₀ X) ≈⟨ sym k-assoc ⟩ + extend (extend idC ∘ idC) ≈⟨ extend-≈ identityʳ ⟩ + extend (extend idC) ≈⟨ extend-≈ (introˡ k-identityʳ) ⟩ + extend ((extend idC ∘ now) ∘ extend idC) ≈⟨ extend-≈ assoc ⟩ + extend (extend idC ∘ now ∘ extend idC) ≈⟨ k-assoc ⟩ + μ.η X ∘ D₁ (μ.η X) ∎ 1⇒2 : cond-1 → cond-2 - 1⇒2 c-1 X = record { s-alg-on = s-alg-on ; ρ-algebra-morphism = begin ρ ∘ μ.η X ≈⟨ D-universal ⟩ Search-Algebra-on.α s-alg-on ∘ D₁ ρ ∎ } + 1⇒2 c-1 X = record { s-alg-on = s-alg-on ; ρ-algebra-morphism = D-universal } where open Coequalizer (coeqs X) renaming (universal to coeq-universal) open IsCoequalizer (c-1 X) using () renaming (equality to D-equality; coequalize to D-coequalize; universal to D-universal; unique to D-unique) @@ -96,18 +123,18 @@ module Monad.Instance.Delay.Properties {o ℓ e} (ambient : Ambient o ℓ e) whe s-alg-on = record { α = α' ; identity₁ = ρ-epi (α' ∘ now) idC (begin - (α' ∘ now) ∘ ρ ≈⟨ pullʳ (η.commute ρ) ⟩ - α' ∘ D₁ ρ ∘ now ≈⟨ pullˡ (sym D-universal) ⟩ + (α' ∘ now) ∘ ρ ≈⟨ pullʳ (η.commute ρ) ⟩ + α' ∘ D₁ ρ ∘ now ≈⟨ pullˡ (sym D-universal) ⟩ (ρ ∘ μ.η X) ∘ now ≈⟨ cancelʳ M-identityʳ ⟩ - ρ ≈⟨ sym identityˡ ⟩ - idC ∘ ρ ∎) + ρ ≈⟨ sym identityˡ ⟩ + idC ∘ ρ ∎) ; identity₂ = IsCoequalizer⇒Epi (c-1 X) (α' ∘ ▷) α' (begin - (α' ∘ ▷) ∘ D₁ ρ ≈⟨ pullʳ (▷∘extend-comm (now ∘ ρ)) ⟩ - α' ∘ D₁ ρ ∘ ▷ ≈⟨ pullˡ (sym D-universal) ⟩ - (ρ ∘ μ.η X) ∘ ▷ ≈⟨ pullʳ (sym (▷∘extend-comm idC)) ⟩ + (α' ∘ ▷) ∘ D₁ ρ ≈⟨ pullʳ (▷∘extend-comm (now ∘ ρ)) ⟩ + α' ∘ D₁ ρ ∘ ▷ ≈⟨ pullˡ (sym D-universal) ⟩ + (ρ ∘ μ.η X) ∘ ▷ ≈⟨ pullʳ (sym (▷∘extend-comm idC)) ⟩ ρ ∘ ▷ ∘ extend idC ≈⟨ pullˡ ρ▷ ⟩ - ρ ∘ extend idC ≈⟨ D-universal ⟩ - α' ∘ D₁ ρ ∎) + ρ ∘ extend idC ≈⟨ D-universal ⟩ + α' ∘ D₁ ρ ∎) } where μ∘Dι : μ.η X ∘ D₁ ι ≈ extend ι @@ -115,14 +142,14 @@ module Monad.Instance.Delay.Properties {o ℓ e} (ambient : Ambient o ℓ e) whe eq₁ : D₁ (extend ι) ≈ D₁ (μ.η X) ∘ D₁ (D₁ ι) eq₁ = sym (begin D₁ (μ.η X) ∘ D₁ (D₁ ι) ≈⟨ sym D-homomorphism ⟩ - D₁ (μ.η X ∘ D₁ ι) ≈⟨ D-resp-≈ μ∘Dι ⟩ - D₁ (extend ι) ∎) + D₁ (μ.η X ∘ D₁ ι) ≈⟨ D-resp-≈ μ∘Dι ⟩ + D₁ (extend ι) ∎) α' = D-coequalize {h = ρ {X} ∘ μ.η X} (begin - (ρ ∘ μ.η X) ∘ D₁ (extend ι) ≈⟨ (refl⟩∘⟨ eq₁) ⟩ + (ρ ∘ μ.η X) ∘ D₁ (extend ι) ≈⟨ (refl⟩∘⟨ eq₁) ⟩ (ρ ∘ μ.η X) ∘ D₁ (μ.η X) ∘ D₁ (D₁ ι) ≈⟨ pullʳ (pullˡ M-assoc) ⟩ ρ ∘ (μ.η X ∘ μ.η (D₀ X)) ∘ D₁ (D₁ ι) ≈⟨ (refl⟩∘⟨ pullʳ (μ.commute ι)) ⟩ - ρ ∘ μ.η X ∘ (D₁ ι) ∘ μ.η (X × N) ≈⟨ (refl⟩∘⟨ pullˡ μ∘Dι) ⟩ - ρ ∘ extend ι ∘ μ.η (X × N) ≈⟨ pullˡ equality ⟩ - (ρ ∘ D₁ π₁) ∘ μ.η (X × N) ≈⟨ (pullʳ (sym (μ.commute π₁)) ○ sym-assoc) ⟩ - (ρ ∘ μ.η X) ∘ D₁ (D₁ π₁) ∎) + ρ ∘ μ.η X ∘ (D₁ ι) ∘ μ.η (X × N) ≈⟨ (refl⟩∘⟨ pullˡ μ∘Dι) ⟩ + ρ ∘ extend ι ∘ μ.η (X × N) ≈⟨ pullˡ equality ⟩ + (ρ ∘ D₁ π₁) ∘ μ.η (X × N) ≈⟨ (pullʳ (sym (μ.commute π₁)) ○ sym-assoc) ⟩ + (ρ ∘ μ.η X) ∘ D₁ (D₁ π₁) ∎) ``` \ No newline at end of file diff --git a/src/Monad/Instance/Delay/Strong.lagda.md b/src/Monad/Instance/Delay/Strong.lagda.md new file mode 100644 index 0000000..36b7122 --- /dev/null +++ b/src/Monad/Instance/Delay/Strong.lagda.md @@ -0,0 +1,305 @@ + + +```agda +module Monad.Instance.Delay.Strong {o ℓ e} (ambient : Ambient o ℓ e) (D : DelayM ambient) where + open Ambient ambient + open HomReasoning + open Equiv + open MR C + open M C + open F-Coalgebra-Morphism renaming (f to u) +``` + +# The Delay Monad is strong + +```agda + module _ where + open DelayM D + open Functor + open RMonad kleisli using (extend; extend-≈) renaming (assoc to k-assoc; identityʳ to k-identityʳ) + open Monad monad using (η; μ) + + -- TODO change 'coinduction' proofs, move the two proofs i.e. f ≈ ! and ! ≈ g to the where clause + + strength : Strength monoidal monad + strength = record + { strengthen = ntHelper (record + { η = τ + ; commute = commute' }) + ; identityˡ = identityˡ' -- triangle + ; η-comm = begin -- η-τ + τ _ ∘ (idC ⁂ now) ≈⟨ refl⟩∘⟨ (⁂-cong₂ (sym identity²) refl ○ sym ⁂∘⁂) ⟩ + τ _ ∘ (idC ⁂ out⁻¹) ∘ (idC ⁂ i₁) ≈⟨ pullˡ (τ-helper _) ⟩ + (out⁻¹ ∘ (idC +₁ τ _) ∘ distributeˡ⁻¹) ∘ (idC ⁂ i₁) ≈⟨ pullʳ (pullʳ dstr-law₁) ⟩ + out⁻¹ ∘ (idC +₁ τ _) ∘ i₁ ≈⟨ refl⟩∘⟨ +₁∘i₁ ⟩ + out⁻¹ ∘ i₁ ∘ idC ≈⟨ refl⟩∘⟨ identityʳ ⟩ + now ∎ + ; μ-η-comm = μ-η-comm' -- μ-τ + ; strength-assoc = strength-assoc' -- square + } + where + out-law : ∀ {X Y} (f : X ⇒ Y) → out {Y} ∘ extend (now ∘ f) ≈ (f +₁ extend (now ∘ f)) ∘ out {X} + out-law {X} {Y} f = begin + out ∘ extend (now ∘ f) ≈⟨ extendlaw (now ∘ f) ⟩ + [ out ∘ now ∘ f , i₂ ∘ extend (now ∘ f) ] ∘ out ≈⟨ ([]-cong₂ (pullˡ unitlaw) refl) ⟩∘⟨refl ⟩ + (f +₁ extend (now ∘ f)) ∘ out ∎ + + -- TODO add to agda-categories + 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₂ + dstr-law₂ = (refl⟩∘⟨ (sym inject₂)) ○ (cancelˡ (IsIso.isoˡ isIsoˡ)) + + module _ (P : Category.Obj (CProduct C C)) where + 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ʳ dstr-law₁) ⟩ + 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ʳ dstr-law₂) ⟩ + 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 })) + + identityˡ' : ∀ {X : Obj} → extend (now ∘ π₂) ∘ τ (Terminal.⊤ terminal , X) ≈ π₂ + identityˡ' {X} = begin + extend (now ∘ π₂) ∘ τ _ ≈⟨ sym (Terminal.!-unique (coalgebras X) {A = record { A = Terminal.⊤ terminal × D₀ X ; α = (π₂ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) }} (record { f = extend (now ∘ π₂) ∘ τ _ ; commutes = begin + out ∘ extend (now ∘ π₂) ∘ τ _ ≈⟨ refl⟩∘⟨ (refl⟩∘⟨ (sym identityʳ)) ⟩ + out ∘ extend (now ∘ π₂) ∘ τ _ ∘ idC ≈⟨ pullˡ diag₃ ⟩ + ((π₂ +₁ extend (now ∘ π₂)) ∘ out) ∘ τ _ ∘ idC ≈⟨ pullʳ (pullˡ (diag₂ (Terminal.⊤ terminal , X))) ⟩ + (π₂ +₁ extend (now ∘ π₂)) ∘ ((idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out)) ∘ idC ≈⟨ refl⟩∘⟨ (pullʳ (assoc ○ sym diag₁)) ⟩ + (π₂ +₁ extend (now ∘ π₂)) ∘ (idC +₁ τ _) ∘ (⟨ Terminal.! terminal , idC ⟩ +₁ idC) ∘ (π₂ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (pullˡ (+₁∘+₁ ○ +₁-cong₂ (_≅_.isoˡ ⊤×A≅A) identity² ○ CC.+-unique ((identity² ⟩∘⟨refl) ○ id-comm-sym) ((identity² ⟩∘⟨refl) ○ id-comm-sym)) ) ⟩ + (π₂ +₁ extend (now ∘ π₂)) ∘ (idC +₁ τ _) ∘ (idC ∘ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ pullˡ +₁∘+₁ ⟩ + (π₂ ∘ idC +₁ extend (now ∘ π₂) ∘ τ _) ∘ (idC ∘ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ (+₁-cong₂ id-comm refl) ⟩∘⟨refl ⟩ + (idC ∘ π₂ +₁ extend (now ∘ π₂) ∘ τ _) ∘ (idC ∘ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈˘⟨ pullˡ +₁∘+₁ ⟩ + (idC +₁ extend (now ∘ π₂)) ∘ (π₂ +₁ τ _) ∘ (idC ∘ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ refl⟩∘⟨ (refl⟩∘⟨ (elimˡ identity²)) ⟩ + (idC +₁ extend (now ∘ π₂)) ∘ (π₂ +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈˘⟨ refl⟩∘⟨ ((+₁-cong₂ identityˡ identityʳ) ⟩∘⟨refl) ⟩ + (idC +₁ extend (now ∘ π₂)) ∘ (idC ∘ π₂ +₁ τ _ ∘ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈˘⟨ pullʳ (pullˡ +₁∘+₁) ⟩ + ((idC +₁ extend (now ∘ π₂)) ∘ (idC +₁ τ _)) ∘ (π₂ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈˘⟨ (homomorphism (X +-)) ⟩∘⟨refl ⟩ + (idC +₁ extend (now ∘ π₂) ∘ τ _) ∘ (π₂ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ∎ })) ⟩ + u (Terminal.! (coalgebras X)) ≈⟨ Terminal.!-unique (coalgebras X) {A = record { A = Terminal.⊤ terminal × D₀ X ; α = (π₂ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) }} (record { f = π₂ ; commutes = begin + out ∘ π₂ ≈˘⟨ π₂∘⁂ ⟩ + π₂ ∘ (idC ⁂ out) ≈˘⟨ pullˡ distribute₂ ⟩ + (π₂ +₁ π₂) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈˘⟨ (+₁-cong₂ identityˡ identityʳ) ⟩∘⟨refl ⟩ + (idC ∘ π₂ +₁ π₂ ∘ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈˘⟨ pullˡ +₁∘+₁ ⟩ + (idC +₁ π₂) ∘ (π₂ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ∎ }) ⟩ + π₂ ∎ + where + diag₁ : (⟨ Terminal.! terminal , idC ⟩ +₁ idC) ∘ (π₂ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈ distributeˡ⁻¹ {Terminal.⊤ terminal} {X} {D₀ X} ∘ (idC ⁂ out) ∘ idC + diag₁ = 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ˡ (CC.+-unique id-comm-sym id-comm-sym) ⟩ + distributeˡ⁻¹ ∘ (idC ⁂ out) ∘ idC ∎ + diag₂ = τ-law + diag₃ : out {X} ∘ extend (now ∘ π₂ {A = Terminal.⊤ terminal} {B = X}) ≈ (π₂ +₁ extend (now ∘ π₂)) ∘ out + diag₃ = out-law π₂ + -- TODO add to agda-categories + distribute₂ : ∀ {A B C} → (π₂ +₁ π₂) ∘ distributeˡ⁻¹ {A} {B} {C} ≈ π₂ + distribute₂ = sym (begin + π₂ ≈⟨ introʳ (IsIso.isoʳ isIsoˡ) ⟩ + π₂ ∘ distributeˡ ∘ distributeˡ⁻¹ ≈⟨ pullˡ ∘[] ⟩ + [ π₂ ∘ ((idC ⁂ i₁)) , π₂ ∘ (idC ⁂ i₂) ] ∘ distributeˡ⁻¹ ≈⟨ ([]-cong₂ π₂∘⁂ π₂∘⁂) ⟩∘⟨refl ⟩ + (π₂ +₁ π₂) ∘ distributeˡ⁻¹ ∎) + + μ-η-comm' : ∀ {X Y} → extend idC ∘ (extend (now ∘ τ _)) ∘ τ _ ≈ τ (X , Y) ∘ (idC ⁂ extend idC) + μ-η-comm' {X} {Y} = begin + extend idC ∘ (extend (now ∘ τ _)) ∘ τ _ ≈⟨ sym (Terminal.!-unique (coalgebras (X × Y)) (record { f = extend idC ∘ (extend (now ∘ τ _)) ∘ τ _ ; commutes = begin + out ∘ extend idC ∘ extend (now ∘ τ (X , Y)) ∘ τ _ ≈⟨ refl⟩∘⟨ (pullˡ id*∘Dτ) ⟩ + out ∘ extend (τ (X , Y)) ∘ τ _ ≈⟨ square ⟩ + [ out ∘ τ _ , i₂ ∘ extend (τ _) ] ∘ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ sym-assoc ○ sym-assoc ○ (assoc ○ tri) ⟩∘⟨refl ⟩ + ((idC +₁ extend (τ _) ∘ τ _) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹) ∘ (idC ⁂ out) ≈⟨ assoc ○ refl⟩∘⟨ assoc ⟩ + (idC +₁ (extend (τ _) ∘ τ _)) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ (+₁-cong₂ refl (sym (pullˡ id*∘Dτ))) ⟩∘⟨refl ⟩ + (idC +₁ (extend idC ∘ extend (now ∘ τ (X , Y)) ∘ τ _)) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ∎ })) ⟩ + u (Terminal.! (coalgebras (X × Y)) {A = record { A = X × D₀ (D₀ Y) ; α = [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) }}) ≈⟨ Terminal.!-unique (coalgebras (X × Y)) (record { f = τ _ ∘ (idC ⁂ extend idC) ; commutes = begin + out ∘ τ _ ∘ (idC ⁂ extend idC) ≈⟨ pullˡ (τ-law (X , Y)) ⟩ + ((idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out)) ∘ (idC ⁂ extend idC) ≈⟨ pullʳ (pullʳ (⁂∘⁂ ○ ⁂-cong₂ identity² refl)) ⟩ + (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out ∘ extend idC) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⁂-cong₂ refl (extendlaw idC) ⟩ + (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ [ out ∘ idC , i₂ ∘ extend idC ] ∘ out) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⁂-cong₂ refl (([]-cong₂ identityʳ refl) ⟩∘⟨refl) ⟩ + (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ [ out , i₂ ∘ extend idC ] ∘ out) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ sym (⁂∘⁂ ○ ⁂-cong₂ identity² refl) ⟩ + (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ [ out , i₂ ∘ extend idC ]) ∘ (idC ⁂ out) ≈⟨ sym-assoc ○ pullˡ (assoc ○ tri₂) ⟩ + ((idC +₁ τ _ ∘ (idC ⁂ extend idC)) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹) ∘ (idC ⁂ out) ≈⟨ assoc ○ refl⟩∘⟨ assoc ⟩ + (idC +₁ τ _ ∘ (idC ⁂ extend idC)) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ∎ }) ⟩ + τ _ ∘ (idC ⁂ extend idC) ∎ + where + -- diagram: https://q.uiver.app/#q=WzAsNyxbMCwwLCJYXFx0aW1lcyBERFkiXSxbMiwwLCJEKFhcXHRpbWVzIERZKSJdLFs0LDAsIkREKFhcXHRpbWVzIFkpIl0sWzAsMiwiWFxcdGltZXMgKERZK0REWSkiXSxbMiwyLCJYXFx0aW1lcyBEWSsgWFxcdGltZXMgRERZIl0sWzQsMiwiWFxcdGltZXMgWSsgREQoWFxcdGltZXMgWSkiXSxbMCw0LCJYXFx0aW1lcyBZKyBYXFx0aW1lcyBERFkiXSxbMCwzLCJpZFxcdGltZXMgb3V0IiwyXSxbMCwxLCJcXHRhdSJdLFsxLDIsIlxcdGF1XioiXSxbMyw0LCIoaWQrXFx0YXUpZGlzdCJdLFs0LDUsIltvdXRcXHRhdSxpbnJcXHRhdV4qXSJdLFsyLDUsIm91dCJdLFsxLDRdLFs2LDUsImlkK1xcdGF1XipcXHRhdSIsMl0sWzMsNiwiWyhpZCArIGlkXFx0aW1lcyBub3cpZGlzdCAoaWRcXHRpbWVzIG91dCksaW5yXWRpc3QiLDJdXQ== + square : out ∘ extend (τ (X , Y)) ∘ τ _ ≈ [ out ∘ τ _ , i₂ ∘ extend (τ _) ] ∘ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) + square = begin + out ∘ extend (τ (X , Y)) ∘ τ _ ≈⟨ pullˡ (extendlaw (τ (X , Y))) ⟩ + ([ out ∘ τ (X , Y) , i₂ ∘ extend (τ (X , Y)) ] ∘ out) ∘ τ _ ≈⟨ pullʳ (τ-law _) ⟩ + [ out ∘ τ _ , i₂ ∘ extend (τ _) ] ∘ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ∎ + tri : [ out ∘ τ _ , i₂ ∘ extend (τ (X , Y)) ] ∘ (idC +₁ τ _) ∘ distributeˡ⁻¹ ≈ (idC +₁ extend (τ _) ∘ τ _) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹ + tri = begin + [ out ∘ τ _ , i₂ ∘ extend (τ (X , Y)) ] ∘ (idC +₁ τ _) ∘ distributeˡ⁻¹ ≈⟨ pullˡ []∘+₁ ⟩ + [ (out ∘ τ _) ∘ idC , (i₂ ∘ extend (τ (X , Y))) ∘ τ _ ] ∘ distributeˡ⁻¹ ≈⟨ ([]-cong₂ (identityʳ ○ τ-law (X , Y)) assoc) ⟩∘⟨refl ⟩ + [ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ∘ extend (τ (X , Y)) ∘ τ _ ] ∘ distributeˡ⁻¹ ≈⟨ sym (([]-cong₂ ((+₁-cong₂ refl k-identityʳ) ⟩∘⟨refl) refl) ⟩∘⟨refl) ⟩ + [ (idC +₁ extend (τ _) ∘ now) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ∘ extend (τ _) ∘ τ _ ] ∘ distributeˡ⁻¹ ≈⟨ sym (([]-cong₂ ((+₁-cong₂ identity² (pullʳ (τ-now (X , D₀ Y)))) ⟩∘⟨refl) refl) ⟩∘⟨refl) ⟩ + [ (idC ∘ idC +₁ (extend (τ _) ∘ τ _) ∘ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ∘ extend (τ _) ∘ τ _ ] ∘ distributeˡ⁻¹ ≈⟨ sym (([]-cong₂ (pullˡ +₁∘+₁) +₁∘i₂) ⟩∘⟨refl) ⟩ + [ (idC +₁ extend (τ _) ∘ τ _) ∘ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , (idC +₁ extend (τ _) ∘ τ _) ∘ i₂ ] ∘ distributeˡ⁻¹ ≈⟨ sym (pullˡ ∘[]) ⟩ + (idC +₁ extend (τ _) ∘ τ _) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹ ∎ + id*∘Dτ : extend idC ∘ extend (now ∘ τ _) ≈ extend (τ _) + id*∘Dτ = begin + extend idC ∘ extend (now ∘ τ _) ≈⟨ sym k-assoc ⟩ + extend (extend idC ∘ now ∘ τ _) ≈⟨ extend-≈ (pullˡ k-identityʳ) ⟩ + extend (idC ∘ τ _) ≈⟨ extend-≈ identityˡ ⟩ + extend (τ _) ∎ + tri₂' : (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ [ out , i₂ ∘ extend idC ]) ∘ [ (idC ⁂ i₁) , (idC ⁂ i₂) ] ≈ (idC +₁ τ _ ∘ (idC ⁂ extend idC)) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹ ∘ distributeˡ + tri₂' = begin + (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ [ out , i₂ ∘ extend idC ]) ∘ [ (idC ⁂ i₁) , (idC ⁂ i₂) ] ≈⟨ refl⟩∘⟨ (refl⟩∘⟨ ∘[]) ⟩ + (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ [ (idC ⁂ [ out , i₂ ∘ extend idC ]) ∘ (idC ⁂ i₁) , (idC ⁂ [ out , i₂ ∘ extend idC ]) ∘ (idC ⁂ i₂) ] ≈⟨ refl⟩∘⟨ refl⟩∘⟨ []-cong₂ ⁂∘⁂ ⁂∘⁂ ⟩ + (idC +₁ τ _) ∘ 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 +₁ τ _) ∘ distributeˡ⁻¹ ∘ [ idC ⁂ out , idC ⁂ i₂ ∘ extend idC ] ≈⟨ refl⟩∘⟨ ∘[] ⟩ + (idC +₁ τ _) ∘ [ distributeˡ⁻¹ ∘ (idC ⁂ out) , distributeˡ⁻¹ ∘ (idC ⁂ i₂ ∘ extend idC) ] ≈⟨ ∘[] ⟩ + [ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ i₂ ∘ extend idC) ] ≈⟨ sym ([]-cong₂ refl (pullʳ (pullʳ (⁂∘⁂ ○ ⁂-cong₂ identity² refl)))) ⟩ + [ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , ((idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ i₂)) ∘ (idC ⁂ extend idC) ] ≈⟨ []-cong₂ refl ((refl⟩∘⟨ dstr-law₂) ⟩∘⟨refl) ⟩ + [ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , ((idC +₁ τ _) ∘ i₂) ∘ (idC ⁂ extend idC) ] ≈⟨ []-cong₂ refl (pushˡ +₁∘i₂) ⟩ + [ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ∘ τ _ ∘ (idC ⁂ extend idC) ] ≈⟨ []-cong₂ ((+₁-cong₂ refl (introʳ (⟨⟩-unique id-comm (id-comm ○ (sym k-identityʳ) ⟩∘⟨refl)))) ⟩∘⟨refl) refl ⟩ + [ (idC +₁ τ _ ∘ (idC ⁂ extend idC ∘ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ∘ τ _ ∘ (idC ⁂ extend idC) ] ≈⟨ []-cong₂ ((sym (+₁-cong₂ refl (refl⟩∘⟨ (⁂∘⁂ ○ ⁂-cong₂ identity² refl)))) ⟩∘⟨refl) refl ⟩ + [ (idC +₁ τ _ ∘ (idC ⁂ extend idC) ∘ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ∘ τ _ ∘ (idC ⁂ extend idC) ] ≈⟨ sym ([]-cong₂ (pullˡ (+₁∘+₁ ○ +₁-cong₂ identity² assoc)) +₁∘i₂) ⟩ + [ (idC +₁ τ _ ∘ (idC ⁂ extend idC)) ∘ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , (idC +₁ τ _ ∘ (idC ⁂ extend idC)) ∘ i₂ ] ≈⟨ sym ∘[] ⟩ + (idC +₁ τ _ ∘ (idC ⁂ extend idC)) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ≈⟨ sym (refl⟩∘⟨ (elimʳ (IsIso.isoˡ isIsoˡ))) ⟩ + (idC +₁ τ _ ∘ (idC ⁂ extend idC)) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹ ∘ distributeˡ ∎ + tri₂ : (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ [ out , i₂ ∘ extend idC ]) ≈ (idC +₁ τ _ ∘ (idC ⁂ extend idC)) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹ + tri₂ = iso-epi-from + (record { from = distributeˡ ; to = distributeˡ⁻¹ ; iso = IsIso.iso isIsoˡ }) + ((idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ [ out , i₂ ∘ extend idC ])) + ((idC +₁ τ _ ∘ (idC ⁂ extend idC)) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹) + (assoc ○ refl⟩∘⟨ assoc ○ tri₂' ○ sym-assoc ○ sym-assoc ○ assoc ⟩∘⟨refl) + + strength-assoc' : ∀ {X Y Z} → extend (now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ τ ((X × Y), Z) ≈ τ _ ∘ (idC ⁂ τ _) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ + strength-assoc' {X} {Y} {Z} = begin + extend (now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ τ _ ≈⟨ sym (Terminal.!-unique (coalgebras (X × Y × Z)) (record { f = extend (now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ τ _ ; commutes = begin + out ∘ extend (now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ τ _ ≈⟨ pullˡ (extendlaw (now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩)) ⟩ + ([ out ∘ now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ , i₂ ∘ extend (now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ] ∘ out) ∘ τ _ ≈⟨ pullʳ (τ-law (X × Y , Z)) ⟩ + [ out ∘ now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ , i₂ ∘ extend (now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ] ∘ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ ([]-cong₂ (pullˡ unitlaw) refl) ⟩∘⟨refl ⟩ + (⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ +₁ extend (now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩)) ∘ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ pullˡ +₁∘+₁ ⟩ + (⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ∘ idC +₁ extend (now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ (+₁-cong₂ id-comm (sym identityʳ)) ⟩∘⟨refl ⟩ + (idC ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ +₁ (extend (now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ τ _) ∘ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ sym (pullˡ +₁∘+₁) ⟩ + (idC +₁ extend (now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ τ _) ∘ (⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ∎ })) ⟩ + u (Terminal.! (coalgebras (X × Y × Z)) {A = record { A = (X × Y) × D₀ Z ; α = (⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) }}) ≈⟨ Terminal.!-unique (coalgebras (X × Y × Z)) (record { f = τ _ ∘ (idC ⁂ τ _) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ; commutes = begin + out ∘ τ _ ∘ (idC ⁂ τ _) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ≈⟨ pullˡ (τ-law (X , Y × Z)) ⟩ + ((idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out)) ∘ (idC ⁂ τ _) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ≈⟨ pullʳ (pullˡ (pullʳ ⁂∘⁂)) ⟩ + (idC +₁ τ _) ∘ (distributeˡ⁻¹ ∘ (idC ∘ idC ⁂ out ∘ τ _)) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ≈⟨ refl⟩∘⟨ assoc ⟩ + (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ∘ idC ⁂ out ∘ τ _) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ≈˘⟨ refl⟩∘⟨ (refl⟩∘⟨ (⁂-cong₂ identityʳ (assoc ○ sym (τ-law (Y , Z)))) ⟩∘⟨refl) ⟩ + (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ ((idC ∘ idC) ∘ idC ⁂ ((idC +₁ τ _) ∘ distributeˡ⁻¹) ∘ (idC ⁂ out)) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ≈⟨ sym (refl⟩∘⟨ (pullʳ (pullˡ ⁂∘⁂ ○ pullˡ ⁂∘⁂))) ⟩ + (idC +₁ τ _) ∘ (distributeˡ⁻¹ ∘ (idC ⁂ (idC +₁ τ _))) ∘ (idC ⁂ distributeˡ⁻¹) ∘ (idC ⁂ (idC ⁂ out)) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ≈⟨ refl⟩∘⟨ (refl⟩∘⟨ (refl⟩∘⟨ helper₁)) ⟩ + (idC +₁ τ _) ∘ (distributeˡ⁻¹ ∘ (idC ⁂ (idC +₁ τ _))) ∘ (idC ⁂ distributeˡ⁻¹) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ∘ (idC ⁂ out) ≈⟨ refl⟩∘⟨ (helper₂ ⟩∘⟨refl) ⟩ + (idC +₁ τ _) ∘ ((idC +₁ (idC ⁂ τ (Y , Z))) ∘ distributeˡ⁻¹) ∘ (idC ⁂ distributeˡ⁻¹) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ∘ (idC ⁂ out) ≈⟨ refl⟩∘⟨ (assoc ○ refl⟩∘⟨ sym assoc²') ⟩ + (idC +₁ τ _) ∘ (idC +₁ (idC ⁂ τ (Y , Z))) ∘ (distributeˡ⁻¹ ∘ (idC ⁂ distributeˡ⁻¹) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ (idC ⁂ out) ≈⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ identity² refl) ⟩ + (idC +₁ τ _ ∘ (idC ⁂ τ (Y , Z))) ∘ (distributeˡ⁻¹ ∘ (idC ⁂ distributeˡ⁻¹) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ (idC ⁂ out) ≈⟨ refl⟩∘⟨ (helper₃ ⟩∘⟨refl) ⟩ + (idC +₁ τ _ ∘ (idC ⁂ τ (Y , Z))) ∘ ((⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ +₁ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ distributeˡ⁻¹) ∘ (idC ⁂ out) ≈⟨ assoc²'' ⟩ + ((idC +₁ τ _ ∘ (idC ⁂ τ _)) ∘ (⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ +₁ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ sym ((+₁-cong₂ refl (identityʳ ○ sym-assoc) ○ sym +₁∘+₁) ⟩∘⟨refl) ⟩ + (idC ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ +₁ (τ _ ∘ (idC ⁂ τ _) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ sym (pullˡ +₁∘+₁) ⟩ + (idC +₁ τ _ ∘ (idC ⁂ τ _) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ (⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ∎ }) ⟩ + τ _ ∘ (idC ⁂ τ _) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ∎ + 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 +₁ τ _)) ≈ (idC +₁ (idC ⁂ τ (Y , Z))) ∘ distributeˡ⁻¹ + helper₂ = sym (distribute₁ idC idC (τ _)) ○ (+₁-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 dstr-law₁))) (⟨⟩-cong₂ identityˡ ((pushˡ (sym dstr-law₂)))) ⟩∘⟨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ˡ⁻¹) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ∎) +-- {- ⁂ ⊤ ○ +-- Diagram for identityˡ': +-- https://q.uiver.app/#q=WzAsOSxbMCwyLCIxIFxcdGltZXMgREIiXSxbMiwyLCIxIFxcdGltZXMgKEIgKyBEQikiXSxbNiwyLCIxIFxcdGltZXMgQiArIDEgXFx0aW1lcyBEQiJdLFswLDQsIkQoMSBcXHRpbWVzIEIpIl0sWzYsNCwiKDEgXFx0aW1lcyBCKSArIEQoMSBcXHRpbWVzIEIpIl0sWzAsNiwiREIiXSxbNiw2LCJCICsgREIiXSxbMCwwLCIxIFxcdGltZXMgREIiXSxbNiwwLCJCICsgMSBcXHRpbWVzIERCIl0sWzAsMSwiaWQgXFx0aW1lcyBvdXQiXSxbMSwyLCJkaXN0cmliXnstMX0iXSxbMCwzLCJcXHRhdSIsMl0sWzUsNiwib3V0IiwyXSxbMyw0LCJvdXQiLDJdLFsyLDQsImlkICsgXFx0YXUiXSxbMyw1LCJEIFxccGlfMiJdLFs0LDYsIlxccGlfMiArIEQgXFxwaV8yIl0sWzcsOCwiKFxccGlfMiArIGlkKSBcXGNpcmMgZGlzdHJpYl57LTF9IFxcY2lyYyAoaWQgXFx0aW1lcyBvdXQpIl0sWzcsMCwiaWQiXSxbOCwyLCJcXGxhbmdsZSAhICwgaWQgXFxyYW5nbGUgKyBpZCJdXQ== +-- -} + 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) = begin + τ _ ∘ (f ⁂ extend (now ∘ g)) ≈⟨ sym (!-unique (record { f = τ _ ∘ (f ⁂ extend (now ∘ g)) ; commutes = 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₁ 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) ∎ })) ⟩ + u ! ≈⟨ !-unique (record { f = extend (now ∘ (f ⁂ g)) ∘ τ _ ; commutes = begin + out ∘ extend (now ∘ (f ⁂ g)) ∘ τ _ ≈⟨ 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 +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ sym-assoc ○ sym-assoc ⟩ + ((((f ⁂ g) +₁ (extend (now ∘ (f ⁂ g)))) ∘ (idC +₁ τ _)) ∘ 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) ∎ }) ⟩ + extend (now ∘ (f ⁂ g)) ∘ τ _ ∎ + where + open Terminal (coalgebras (W × X)) + alg' : F-Coalgebra ((W × X) +-) + alg' = record { A = U × D₀ V ; α = ((f ⁂ g) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) } + + strongMonad : StrongMonad monoidal + strongMonad = record { M = monad ; strength = strength } +```