From 7c5dccc0abfc913a2746717e994960b979db2fac Mon Sep 17 00:00:00 2001
From: Leon Vatthauer <leon.vatthauer@fau.de>
Date: Thu, 21 Sep 2023 22:34:38 +0200
Subject: [PATCH] Worked on strength of delay
---
.../Instance/AmbientCategory.lagda.md | 13 +
src/Monad/Instance/Delay.lagda.md | 289 ++++++++++++------
2 files changed, 205 insertions(+), 97 deletions(-)
diff --git a/src/Category/Instance/AmbientCategory.lagda.md b/src/Category/Instance/AmbientCategory.lagda.md
index fd2d782..db4a496 100644
--- a/src/Category/Instance/AmbientCategory.lagda.md
+++ b/src/Category/Instance/AmbientCategory.lagda.md
@@ -9,6 +9,8 @@ open import Categories.Category.Distributive using (Distributive)
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.Monoidal
open import Categories.Category.Cocartesian using (Cocartesian)
open import Categories.Object.NaturalNumbers.Parametrized using (ParametrizedNNO)
open import Categories.Object.Exponential using (Exponential)
@@ -43,6 +45,8 @@ module Category.Instance.AmbientCategory where
open Extensive extensive public
open Cocartesian cocartesian renaming (+-unique to []-unique) public
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
open BinaryProducts products renaming (η to ⁂-η; g-η to ⁂-g-η; unique to ⟨⟩-unique; unique′ to ⟨⟩-unique′) public
@@ -52,7 +56,16 @@ module Category.Instance.AmbientCategory where
distributive : Distributive C
distributive = Extensive×Cartesian⇒Distributive C extensive cartesian
open Distributive distributive hiding (cartesian; cocartesian) public
+ open M' C
+
+ distributeˡ⁻¹ : ∀ {A B C : Obj} → A × (B + C) ⇒ A × B + A × C
+ distributeˡ⁻¹ = IsIso.inv isIsoˡ
+ distributeʳ⁻¹ : ∀ {A B C : Obj} → (B + C) × A ⇒ B × A + C × A
+ distributeʳ⁻¹ = IsIso.inv isIsoʳ
+
+
+
module M = M'
module MR = MR'
```
\ No newline at end of file
diff --git a/src/Monad/Instance/Delay.lagda.md b/src/Monad/Instance/Delay.lagda.md
index 4599027..bce4d1b 100644
--- a/src/Monad/Instance/Delay.lagda.md
+++ b/src/Monad/Instance/Delay.lagda.md
@@ -7,10 +7,12 @@ open import Categories.Object.Terminal
open import Categories.Category.Construction.F-Coalgebras
open import Categories.Category.Construction.F-Algebras
open import Categories.Functor.Coalgebra
-open import Categories.Functor
+open import Categories.Functor renaming (id to idF)
open import Categories.Functor.Algebra
open import Categories.Monad.Construction.Kleisli
+open import Categories.Monad.Strong
open import Categories.Category.Construction.F-Coalgebras
+open import Categories.NaturalTransformation
open import Category.Instance.AmbientCategory using (Ambient)
```
-->
@@ -121,11 +123,86 @@ and second that `extend f` is the unique morphism satisfying the commutative dia
D₀ : Obj → Obj
D₀ X = DX {X}
+ module _ {X Y : Obj} (f : X ⇒ D₀ Y) where
+ open Terminal
+ alg : F-Coalgebra (Y +-)
+ alg = record { A = D₀ X + D₀ Y ; α = [ [ [ i₁ , i₂ ∘ i₂ ] ∘ (out ∘ f) , i₂ ∘ i₁ ] ∘ out , (idC +₁ i₂) ∘ out ] }
+
+ extend' : D₀ X ⇒ D₀ Y
+ extend' = u (! (coalgebras Y) {A = alg}) ∘ i₁ {B = D₀ Y}
+
+ !∘i₂ : u (! (coalgebras Y) {A = alg}) ∘ i₂ ≈ idC
+ !∘i₂ = ⊤-id (coalgebras Y) (F-Coalgebras (Y +-) [ ! (coalgebras Y) ∘ record { f = i₂ ; commutes = inject₂ } ] )
+
+ extendlaw : out ∘ extend' ≈ [ out ∘ f , i₂ ∘ extend' ] ∘ out
+ extendlaw = begin
+ out ∘ extend' ≈⟨ pullˡ (commutes (! (coalgebras Y) {A = alg})) ⟩
+ ((idC +₁ (u (! (coalgebras Y)))) ∘ α alg) ∘ i₁ ≈⟨ pullʳ inject₁ ⟩
+ (idC +₁ (u (! (coalgebras Y)))) ∘ [ [ i₁ , i₂ ∘ i₂ ]
+ ∘ (out ∘ f) , i₂ ∘ i₁ ] ∘ out ≈⟨ pullˡ ∘[] ⟩
+ [ (idC +₁ (u (! (coalgebras Y)))) ∘ [ i₁ , i₂ ∘ i₂ ] ∘ (out ∘ f)
+ , (idC +₁ (u (! (coalgebras Y)))) ∘ i₂ ∘ i₁ ] ∘ out ≈⟨ ([]-cong₂ (pullˡ ∘[]) (pullˡ +₁∘i₂)) ⟩∘⟨refl ⟩
+ [ [ (idC +₁ (u (! (coalgebras Y)))) ∘ i₁
+ , (idC +₁ (u (! (coalgebras Y)))) ∘ i₂ ∘ i₂ ] ∘ (out ∘ f)
+ , (i₂ ∘ (u (! (coalgebras Y)))) ∘ i₁ ] ∘ out ≈⟨ ([]-cong₂
+ (([]-cong₂ +₁∘i₁ (pullˡ +₁∘i₂)) ⟩∘⟨refl)
+ refl) ⟩∘⟨refl ⟩
+ [ [ i₁ ∘ idC , (i₂ ∘ (u (! (coalgebras Y)))) ∘ i₂ ] ∘ (out ∘ f)
+ , (i₂ ∘ (u (! (coalgebras Y)))) ∘ i₁ ] ∘ out ≈⟨ ([]-cong₂
+ (elimˡ (([]-cong₂ identityʳ (cancelʳ !∘i₂)) ○ +-η))
+ assoc) ⟩∘⟨refl ⟩
+ [ out ∘ f , i₂ ∘ extend' ] ∘ out ∎
+
+ extend'-unique : (g : D₀ X ⇒ D₀ Y) → (out ∘ g ≈ [ out ∘ f , i₂ ∘ g ] ∘ out) → extend' ≈ g
+ extend'-unique g g-commutes = begin
+ extend' ≈⟨ (!-unique (coalgebras Y) (record { f = [ g , idC ] ; commutes = begin
+ out ∘ [ g , idC ] ≈⟨ ∘[] ⟩
+ [ out ∘ g , out ∘ idC ] ≈⟨ []-cong₂ g-commutes identityʳ ⟩
+ [ [ out ∘ f , i₂ ∘ g ] ∘ out , out ] ≈˘⟨ []-cong₂
+ (([]-cong₂
+ (([]-cong₂ refl identityʳ) ⟩∘⟨refl ○ (elimˡ +-η))
+ refl)
+ ⟩∘⟨refl)
+ refl ⟩
+ [ [ [ i₁ , i₂ ∘ idC ] ∘ (out ∘ f)
+ , i₂ ∘ g ] ∘ out
+ , out ] ≈˘⟨ []-cong₂
+ (([]-cong₂
+ (([]-cong₂ identityʳ (pullʳ inject₂)) ⟩∘⟨refl)
+ refl)
+ ⟩∘⟨refl)
+ refl
+ ⟩
+ [ [ [ i₁ ∘ idC
+ , (i₂ ∘ [ g , idC ]) ∘ i₂ ] ∘ (out ∘ f)
+ , i₂ ∘ g ] ∘ out
+ , out ] ≈˘⟨ []-cong₂
+ (([]-cong₂
+ (([]-cong₂ +₁∘i₁ (pullˡ +₁∘i₂)) ⟩∘⟨refl)
+ (pullʳ inject₁))
+ ⟩∘⟨refl)
+ (elimˡ (Functor.identity (Y +-)))
+ ⟩
+ [ [ [ (idC +₁ [ g , idC ]) ∘ i₁
+ , (idC +₁ [ g , idC ]) ∘ i₂ ∘ i₂ ] ∘ (out ∘ f)
+ , (i₂ ∘ [ g , idC ]) ∘ i₁ ] ∘ out
+ , (idC +₁ idC) ∘ out ] ≈˘⟨ []-cong₂
+ (([]-cong₂ (pullˡ ∘[]) (pullˡ +₁∘i₂)) ⟩∘⟨refl)
+ ((+₁-cong₂ identity² inject₂) ⟩∘⟨refl) ⟩
+ [ [ (idC +₁ [ g , idC ]) ∘ [ i₁ , i₂ ∘ i₂ ] ∘ (out ∘ f)
+ , (idC +₁ [ g , idC ]) ∘ i₂ ∘ i₁ ] ∘ out
+ , (idC ∘ idC +₁ [ g , idC ] ∘ i₂) ∘ out ] ≈˘⟨ []-cong₂ (pullˡ ∘[]) (pullˡ +₁∘+₁) ⟩
+ [ (idC +₁ [ g , idC ]) ∘ [ [ i₁ , i₂ ∘ i₂ ] ∘ (out ∘ f) , i₂ ∘ i₁ ] ∘ out
+ , (idC +₁ [ g , idC ]) ∘ (idC +₁ i₂) ∘ out ] ≈˘⟨ ∘[] ⟩
+ (idC +₁ [ g , idC ]) ∘ α alg ∎ })) ⟩∘⟨refl ⟩
+ [ g , idC ] ∘ i₁ ≈⟨ inject₁ ⟩
+ g ∎
+
kleisli : KleisliTriple C
kleisli = record
{ F₀ = D₀
; unit = now
- ; extend = extend
+ ; extend = extend'
; identityʳ = identityʳ'
; identityˡ = identityˡ'
; assoc = assoc'
@@ -134,79 +211,6 @@ and second that `extend f` is the unique morphism satisfying the commutative dia
}
where
open Terminal
- module _ {X Y : Obj} (f : X ⇒ D₀ Y) where
- alg : F-Coalgebra (Y +-)
- alg = record { A = D₀ X + D₀ Y ; α = [ [ [ i₁ , i₂ ∘ i₂ ] ∘ (out ∘ f) , i₂ ∘ i₁ ] ∘ out , (idC +₁ i₂) ∘ out ] }
-
- extend : D₀ X ⇒ D₀ Y
- extend = u (! (coalgebras Y) {A = alg}) ∘ i₁ {B = D₀ Y}
-
- !∘i₂ : u (! (coalgebras Y) {A = alg}) ∘ i₂ ≈ idC
- !∘i₂ = ⊤-id (coalgebras Y) (F-Coalgebras (Y +-) [ ! (coalgebras Y) ∘ record { f = i₂ ; commutes = inject₂ } ] )
-
- extendlaw : out ∘ extend ≈ [ out ∘ f , i₂ ∘ extend ] ∘ out
- extendlaw = begin
- out ∘ extend ≈⟨ pullˡ (commutes (! (coalgebras Y) {A = alg})) ⟩
- ((idC +₁ (u (! (coalgebras Y)))) ∘ α alg) ∘ i₁ ≈⟨ pullʳ inject₁ ⟩
- (idC +₁ (u (! (coalgebras Y)))) ∘ [ [ i₁ , i₂ ∘ i₂ ]
- ∘ (out ∘ f) , i₂ ∘ i₁ ] ∘ out ≈⟨ pullˡ ∘[] ⟩
- [ (idC +₁ (u (! (coalgebras Y)))) ∘ [ i₁ , i₂ ∘ i₂ ] ∘ (out ∘ f)
- , (idC +₁ (u (! (coalgebras Y)))) ∘ i₂ ∘ i₁ ] ∘ out ≈⟨ ([]-cong₂ (pullˡ ∘[]) (pullˡ +₁∘i₂)) ⟩∘⟨refl ⟩
- [ [ (idC +₁ (u (! (coalgebras Y)))) ∘ i₁
- , (idC +₁ (u (! (coalgebras Y)))) ∘ i₂ ∘ i₂ ] ∘ (out ∘ f)
- , (i₂ ∘ (u (! (coalgebras Y)))) ∘ i₁ ] ∘ out ≈⟨ ([]-cong₂
- (([]-cong₂ +₁∘i₁ (pullˡ +₁∘i₂)) ⟩∘⟨refl)
- refl) ⟩∘⟨refl ⟩
- [ [ i₁ ∘ idC , (i₂ ∘ (u (! (coalgebras Y)))) ∘ i₂ ] ∘ (out ∘ f)
- , (i₂ ∘ (u (! (coalgebras Y)))) ∘ i₁ ] ∘ out ≈⟨ ([]-cong₂
- (elimˡ (([]-cong₂ identityʳ (cancelʳ !∘i₂)) ○ +-η))
- assoc) ⟩∘⟨refl ⟩
- [ out ∘ f , i₂ ∘ extend ] ∘ out ∎
-
- extend-unique : (g : D₀ X ⇒ D₀ Y) → (out ∘ g ≈ [ out ∘ f , i₂ ∘ g ] ∘ out) → extend ≈ g
- extend-unique g g-commutes = begin
- extend ≈⟨ (!-unique (coalgebras Y) (record { f = [ g , idC ] ; commutes = begin
- out ∘ [ g , idC ] ≈⟨ ∘[] ⟩
- [ out ∘ g , out ∘ idC ] ≈⟨ []-cong₂ g-commutes identityʳ ⟩
- [ [ out ∘ f , i₂ ∘ g ] ∘ out , out ] ≈˘⟨ []-cong₂
- (([]-cong₂
- (([]-cong₂ refl identityʳ) ⟩∘⟨refl ○ (elimˡ +-η))
- refl)
- ⟩∘⟨refl)
- refl ⟩
- [ [ [ i₁ , i₂ ∘ idC ] ∘ (out ∘ f)
- , i₂ ∘ g ] ∘ out
- , out ] ≈˘⟨ []-cong₂
- (([]-cong₂
- (([]-cong₂ identityʳ (pullʳ inject₂)) ⟩∘⟨refl)
- refl)
- ⟩∘⟨refl)
- refl
- ⟩
- [ [ [ i₁ ∘ idC
- , (i₂ ∘ [ g , idC ]) ∘ i₂ ] ∘ (out ∘ f)
- , i₂ ∘ g ] ∘ out
- , out ] ≈˘⟨ []-cong₂
- (([]-cong₂
- (([]-cong₂ +₁∘i₁ (pullˡ +₁∘i₂)) ⟩∘⟨refl)
- (pullʳ inject₁))
- ⟩∘⟨refl)
- (elimˡ (Functor.identity (Y +-)))
- ⟩
- [ [ [ (idC +₁ [ g , idC ]) ∘ i₁
- , (idC +₁ [ g , idC ]) ∘ i₂ ∘ i₂ ] ∘ (out ∘ f)
- , (i₂ ∘ [ g , idC ]) ∘ i₁ ] ∘ out
- , (idC +₁ idC) ∘ out ] ≈˘⟨ []-cong₂
- (([]-cong₂ (pullˡ ∘[]) (pullˡ +₁∘i₂)) ⟩∘⟨refl)
- ((+₁-cong₂ identity² inject₂) ⟩∘⟨refl) ⟩
- [ [ (idC +₁ [ g , idC ]) ∘ [ i₁ , i₂ ∘ i₂ ] ∘ (out ∘ f)
- , (idC +₁ [ g , idC ]) ∘ i₂ ∘ i₁ ] ∘ out
- , (idC ∘ idC +₁ [ g , idC ] ∘ i₂) ∘ out ] ≈˘⟨ []-cong₂ (pullˡ ∘[]) (pullˡ +₁∘+₁) ⟩
- [ (idC +₁ [ g , idC ]) ∘ [ [ i₁ , i₂ ∘ i₂ ] ∘ (out ∘ f) , i₂ ∘ i₁ ] ∘ out
- , (idC +₁ [ g , idC ]) ∘ (idC +₁ i₂) ∘ out ] ≈˘⟨ ∘[] ⟩
- (idC +₁ [ g , idC ]) ∘ α alg ∎ })) ⟩∘⟨refl ⟩
- [ g , idC ] ∘ i₁ ≈⟨ inject₁ ⟩
- g ∎
αf≈αg : ∀ {X Y} {f g : X ⇒ D₀ Y} → f ≈ g → α (alg f) ≈ α (alg g)
αf≈αg {X} {Y} {f} {g} eq = []-cong₂ ([]-cong₂ (refl⟩∘⟨ refl⟩∘⟨ eq) refl ⟩∘⟨refl) refl
@@ -230,18 +234,18 @@ and second that `extend f` is the unique morphism satisfying the commutative dia
}
where open Functor (Y +-) using (identity)
- identityʳ' : ∀ {X Y : Obj} {f : X ⇒ D₀ Y} → extend f ∘ now {X} ≈ f
+ 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 ∎
- 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}))) ⟩
+ 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})))
∘ [ [ i₁ , i₂ ∘ i₂ ] ∘ (out ∘ now) , i₂ ∘ i₁ ] ∘ out ≈⟨ refl⟩∘⟨ []-cong₂ ((refl⟩∘⟨ unitlaw) ○ inject₁) refl ⟩∘⟨refl ⟩
@@ -249,21 +253,21 @@ and second that `extend f` is the unique morphism satisfying the commutative dia
[ (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 ∘ 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 ∎)
+ 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 ∘ 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 ∎)
- extend-≈' : ∀ {X} {Y} {f g : X ⇒ D₀ Y} → f ≈ g → extend f ≈ extend g
+ 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ʳ ⟩
@@ -272,7 +276,7 @@ and second that `extend f` is the unique morphism satisfying the commutative dia
(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
@@ -281,3 +285,94 @@ 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)
+ open import Categories.Category.Product renaming (Product to CProduct; _⁂_ to _×C_)
+ strength : Strength monoidal monad
+ strength = record
+ { strengthen = ntHelper (record
+ { η = τ
+ ; commute = commute' })
+ ; identityˡ = λ {X} → begin
+ extend (now ∘ π₂) ∘ τ _ ≈⟨ introˡ (_≅_.isoˡ out-≅) ⟩
+ (out⁻¹ ∘ out) ∘ extend (now ∘ π₂) ∘ τ _ ≈⟨ pullʳ (pullˡ (extendlaw (now ∘ π₂))) ⟩
+ out⁻¹ ∘ ([ out ∘ now ∘ π₂ , i₂ ∘ extend (now ∘ π₂)] ∘ out) ∘ τ _ ≈⟨ refl⟩∘⟨ (pullʳ (τ-law (Terminal.⊤ terminal , X))) ⟩
+ out⁻¹ ∘ [ out ∘ now ∘ π₂ , i₂ ∘ extend (now ∘ π₂)] ∘ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ {! refl⟩∘⟨_ !} ⟩
+ {! !} ≈⟨ {! !} ⟩
+ {! !} ≈⟨ {! !} ⟩
+ {! !} ≈⟨ {! !} ⟩
+ {! !} ≈⟨ {! !} ⟩
+ -- TODO extend and τ are both final coalgebras, maybe use this?
+ π₂ ∎
+ ; η-comm = {! !}
+ ; μ-η-comm = {! !}
+ ; strength-assoc = {! !}
+ }
+ where
+ open import Agda.Builtin.Sigma
+ 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) }})
+
+ τ-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 }))
+
+ 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) }
+ distribute₁ : ∀ {X Y Z U V W} (f : X ⇒ U) (g : Y ⇒ V) (h : Z ⇒ W) → ((f ⁂ g) +₁ (f ⁂ h)) ∘ distributeˡ⁻¹ ≈ distributeˡ⁻¹ ∘ (f ⁂ (g +₁ h))
+ distribute₁ f g h = begin
+ ((f ⁂ g) +₁ (f ⁂ h)) ∘ distributeˡ⁻¹ ≈⟨ introˡ (IsIso.isoˡ isIsoˡ) ⟩
+ (distributeˡ⁻¹ ∘ distributeˡ) ∘ ((f ⁂ g) +₁ (f ⁂ h)) ∘ distributeˡ⁻¹ ≈⟨ pullˡ (pullʳ []∘+₁) ⟩
+ (distributeˡ⁻¹ ∘ [(idC ⁂ i₁) ∘ (f ⁂ g) , (idC ⁂ i₂) ∘ (f ⁂ h)]) ∘ distributeˡ⁻¹ ≈⟨ (refl⟩∘⟨ ([]-cong₂ ⁂∘⁂ ⁂∘⁂)) ⟩∘⟨refl ⟩
+ (distributeˡ⁻¹ ∘ [ idC ∘ f ⁂ i₁ ∘ g , idC ∘ f ⁂ i₂ ∘ h ]) ∘ distributeˡ⁻¹ ≈⟨ sym ((refl⟩∘⟨ ([]-cong₂ (⁂-cong₂ id-comm +₁∘i₁) (⁂-cong₂ id-comm +₁∘i₂))) ⟩∘⟨refl) ⟩
+ (distributeˡ⁻¹ ∘ [ f ∘ idC ⁂ (g +₁ h) ∘ i₁ , f ∘ idC ⁂ (g +₁ h) ∘ i₂ ]) ∘ distributeˡ⁻¹ ≈˘⟨ (refl⟩∘⟨ ([]-cong₂ ⁂∘⁂ ⁂∘⁂)) ⟩∘⟨refl ⟩
+ (distributeˡ⁻¹ ∘ [ ((f ⁂ (g +₁ h)) ∘ (idC ⁂ i₁)) , ((f ⁂ (g +₁ h)) ∘ (idC ⁂ i₂)) ]) ∘ distributeˡ⁻¹ ≈⟨ sym (pullˡ (pullʳ ∘[])) ⟩
+ (distributeˡ⁻¹ ∘ (f ⁂ (g +₁ h))) ∘ distributeˡ ∘ distributeˡ⁻¹ ≈⟨ sym (introʳ (IsIso.isoʳ isIsoˡ)) ⟩
+ distributeˡ⁻¹ ∘ (f ⁂ (g +₁ h)) ∎
+-- ⁂ ○ ˡ
+ strongMonad : StrongMonad monoidal
+ strongMonad = record { M = monad ; strength = strength }
+```
+