use coproduct functor from library, minor changes

src/Monad/Instance/Delay.lagda.md

@@ -58,25 +58,13 @@ module Monad.Instance.Delay {o ℓ e} (ED : ExtensiveDistributiveCategory o ℓ
 ```
 -->
 
-The delay monad is described via existence of final (Y + \_)-coalgebras, so first we need to define the (Y + \_)-functor:
+The Delay monad is usually described by existence of final coalgebras for the functor `(X + -)` where `X` is some arbitrary object.
-
+This functor trivially sends objects `Y` to `X + Y` and functions `f` to `id + f`.
-```agda
-  delayF : Obj → Endofunctor C
-  delayF Y = record
-    { F₀ = Y +_
-    ; F₁ = idC +₁_
-    ; identity = CC.coproduct.unique id-comm-sym id-comm-sym
-    ; homomorphism = ⟺ (+₁∘+₁ ○ +₁-cong₂ identity² refl) 
-    ; F-resp-≈ = +₁-cong₂ refl
-    }
-```
-
-Using this functor we can define the delay monad ***D***:
 
 ```agda
   record DelayM : Set (o ⊔ ℓ ⊔ e) where
     field
-      coalgebras : ∀ (A : Obj) → Terminal (F-Coalgebras (delayF A))
+      coalgebras : ∀ (A : Obj) → Terminal (F-Coalgebras (A +-))
 ```
 
 These are all the fields this record needs! 
@@ -94,7 +82,7 @@ We can now define these functions by bisecting the isomorphism `out : DX ≅ X +
       D₀ = DX
 
       out-≅ : DX ≅ X + DX
-      out-≅ = colambek {F = delayF X} (coalgebras X)
+      out-≅ = colambek {F = X +- } (coalgebras X)
 
       -- note: out-≅.from ≡ ⊤.α
       open _≅_ out-≅ using () renaming (to to out⁻¹; from to out) public
@@ -109,8 +97,10 @@ We can now define these functions by bisecting the isomorphism `out : DX ≅ X +
       unitlaw = cancelˡ (_≅_.isoʳ out-≅)
 ```
 
-Since `DX` is part of a final coalgebra, we can define a *coiteration operator* that sends every `Y ⇒ X + Y` to `Y ⇒ DX` for an arbitrary `Y`
+Since `Y ⇒ X + Y` is an algebra for the `(X + -)` functor, we can use our terminal coalgebras to get a *coiteration operator* `coit`:
-TODO rephrase, add diagram
+
+TODO add diagram
+
 ```agda
       module _ {Y : Obj} where 
         coit : Y ⇒ X + Y → Y ⇒ DX
@@ -120,8 +110,8 @@ TODO rephrase, add diagram
         coit-commutes f = commutes (! {A = record { A = Y ; α = f }})
 ```
 
-If we combine the interal algebra structure of Parametrized NNOs with Lambek's lemma, we get the isomorphism `X × N ≅ X + X × N`.
+If we combine the internal algebra structure of Parametrized NNOs with Lambek's lemma, we get the isomorphism `X × N ≅ X + X × N`.
-At the same time the morphism `X × N ⇒ X + X × N` is a coalgebra for the `delayF` defined above, this gives us another morphism `ι : X × N ⇒ DX` by using the final coalgebras.
+At the same time the morphism `X × N ⇒ X + X × N` is a coalgebra for the `(Y + \_)`-functor defined above, this gives us another morphism `ι : X × N ⇒ DX` by using the final coalgebras.
 TODO add diagram
 
 ```agda
@@ -157,14 +147,14 @@ TODO
       where
         open Terminal
         module _ {X Y : Obj} (f : X ⇒ D₀ Y) where
-          alg : F-Coalgebra (delayF Y)
+          alg : F-Coalgebra (Y +-)
           alg = record { A = D₀ X + D₀ Y ; α = [ [ [ i₁ , i₂ ∘ i₂ ] ∘ (out Y ∘ f) , i₂ ∘ i₁ ] ∘ out X , (idC +₁ i₂) ∘ out Y ] }
 
           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 (delayF Y) [ ! (coalgebras Y) ∘ record { f = i₂ ; commutes = inject₂ } ] )
+          !∘i₂ = ⊤-id (coalgebras Y) (F-Coalgebras (Y +-) [ ! (coalgebras Y) ∘ record { f = i₂ ; commutes = inject₂ } ] )
 
           extendlaw : out Y ∘ extend ≈ [ out Y ∘ f , i₂ ∘ extend ] ∘ out X
           extendlaw = begin 
@@ -213,7 +203,7 @@ TODO
                                                                                   (([]-cong₂ +₁∘i₁ (pullˡ +₁∘i₂)) ⟩∘⟨refl) 
                                                                                   (pullʳ inject₁)) 
                                                                                 ⟩∘⟨refl) 
-                                                                                (elimˡ (Functor.identity (delayF Y))) 
+                                                                                (elimˡ (Functor.identity (Y +-))) 
                                                                               ⟩
               [ [ [ (idC +₁ [ g , idC ]) ∘ i₁ 
                   , (idC +₁ [ g , idC ]) ∘ i₂ ∘ i₂ ] ∘ (out Y ∘ f) 
@@ -233,7 +223,7 @@ TODO
         α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
 
-        alg-f≈alg-g : ∀ {X Y} {f g : X ⇒ D₀ Y} → f ≈ g → M._≅_ (F-Coalgebras (delayF Y)) (alg f) (alg g)
+        alg-f≈alg-g : ∀ {X Y} {f g : X ⇒ D₀ Y} → f ≈ g → M._≅_ (F-Coalgebras (Y +-)) (alg f) (alg g)
         alg-f≈alg-g {X} {Y} {f} {g} eq = record 
           { from = record { f = idC ; commutes = begin 
             α (alg g) ∘ idC          ≈⟨ identityʳ ⟩ 
@@ -250,7 +240,7 @@ TODO
             ; isoʳ = identity² 
             } 
           }
-          where open Functor (delayF Y) using (identity)
+          where open Functor (Y +-) using (identity)
 
         identityʳ' : ∀ {X} {Y} {f} → extend f ∘ now X ≈ f
         identityʳ' {X} {Y} {f} = begin 
@@ -290,7 +280,7 @@ TODO
           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-≈ (delayF Y) identityʳ ⟩∘⟨ αf≈αg eq ⟩ 
+            (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 ⟩