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 } +``` +