bsc-leon-vatthauer/src/Monad/Instance/Delay.lagda.md

<!--
```agda
{-# OPTIONS --allow-unsolved-metas #-}
open import Level
open import Categories.Category
open import Categories.Monad
open import Categories.Category.Distributive
open import Categories.Category.Extensive.Bundle
open import Categories.Category.Extensive
open import Categories.Category.BinaryProducts
open import Categories.Category.Cocartesian
open import Categories.Category.Cartesian
open import Categories.Category.Cartesian
open import Categories.Object.Terminal
open import Categories.Object.Coproduct
open import Categories.Category.Construction.F-Coalgebras
open import Categories.Functor.Coalgebra
open import Categories.Functor
open import Categories.Functor.Algebra
open import Categories.Monad.Construction.Kleisli
open import Categories.Category.Construction.F-Coalgebras
open import Categories.NaturalTransformation
import Categories.Morphism as M
import Categories.Morphism.Reasoning as MR
```
-->

## Summary
This file introduces the delay monad ***D***

- [ ] *Proposition 1* Characterization of the delay monad ***D***
- [ ] *Proposition 2* ***D*** is commutative

## Code

```agda
module Monad.Instance.Delay {o ℓ e} (ED : ExtensiveDistributiveCategory o ℓ e) where
  open ExtensiveDistributiveCategory ED renaming (U to C; id to idC)
  open Cocartesian (Extensive.cocartesian extensive)
  open Cartesian (ExtensiveDistributiveCategory.cartesian ED)
  open BinaryProducts products

  open M C
  open MR C
  open Equiv
  open HomReasoning
  open CoLambek
```
### *Proposition 1*: Characterization of the delay monad ***D***

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

  record DelayM : Set (o ⊔ ℓ ⊔ e) where
    field
      algebras : ∀ (A : Obj) → Terminal (F-Coalgebras (delayF A))
    
    module D A = Functor (delayF A)

    module _ (X : Obj) where
      open Terminal (algebras X) using (⊤; !)
      open F-Coalgebra ⊤ renaming (A to DX)

      D₀ = DX

      out-≅ : DX ≅ X + DX
      out-≅ = colambek {F = delayF X} (algebras X)

      -- note: out-≅.from ≡ ⊤.α
      open _≅_ out-≅ using () renaming (to to out⁻¹; from to out) public

      now : X ⇒ DX
      now = out⁻¹ ∘ i₁

      later : DX ⇒ DX
      later = out⁻¹ ∘ i₂

      -- TODO inline
      unitlaw : out ∘ now ≈ i₁
      unitlaw = cancelˡ (_≅_.isoʳ out-≅)

      module _ {Y : Obj} where 
        coit : Y ⇒ X + Y → Y ⇒ DX
        coit f = F-Coalgebra-Morphism.f (! {A = record { A = Y ; α = f }})

        coit-commutes : ∀ (f : Y ⇒ X + Y) → out ∘ (coit f) ≈ (idC +₁ coit f) ∘ f
        coit-commutes f = F-Coalgebra-Morphism.commutes (! {A = record { A = Y ; α = f }})

    monad : Monad C
    monad = Kleisli⇒Monad C (record
      { F₀ = D₀ 
      ; unit = λ {X} → now X
      ; extend = extend
      ; identityʳ = λ {X} {Y} {f} → begin 
        extend f ∘ now X                                          ≈⟨ (insertˡ (_≅_.isoˡ (out-≅ Y))) ⟩∘⟨refl ⟩ 
        (out⁻¹ Y ∘ out Y ∘ extend f) ∘ now X                      ≈⟨ (refl⟩∘⟨ (extendlaw f)) ⟩∘⟨refl ⟩
        (out⁻¹ Y ∘ [ out Y ∘ f , i₂ ∘ extend f ] ∘ out X) ∘ now X ≈⟨ pullʳ (pullʳ (unitlaw X)) ⟩
        out⁻¹ Y ∘ [ out Y ∘ f , i₂ ∘ extend f ] ∘ i₁              ≈⟨ refl⟩∘⟨ inject₁ ⟩
        out⁻¹ Y ∘ out Y ∘ f                                       ≈⟨ cancelˡ (_≅_.isoˡ (out-≅ Y)) ⟩
        f                                                         ∎
      ; identityˡ = λ {X} → Terminal.⊤-id (algebras X) (record { f = extend (now X) ; commutes = begin 
        out X ∘ extend (now X)                                                                                             ≈⟨ pullˡ ((F-Coalgebra-Morphism.commutes (Terminal.! (algebras X) {A = alg (now X)}))) ⟩ 
        ((idC +₁ (F-Coalgebra-Morphism.f (Terminal.! (algebras X) {A = alg (now X)}))) ∘ F-Coalgebra.α (alg (now X))) ∘ i₁ ≈⟨ pullʳ inject₁ ⟩
        (idC +₁ (F-Coalgebra-Morphism.f (Terminal.! (algebras X) {A = alg (now X)}))) 
        ∘ [ [ i₁ , i₂ ∘ i₂ ] ∘ (out X ∘ (now X)) , i₂ ∘ i₁ ] ∘ out X                                                       ≈⟨ refl⟩∘⟨ []-cong₂ ((refl⟩∘⟨ (unitlaw X)) ○ inject₁) refl ⟩∘⟨refl ⟩
        (idC +₁ (F-Coalgebra-Morphism.f (Terminal.! (algebras X) {A = alg (now X)}))) ∘ [ i₁ , i₂ ∘ i₁ ] ∘ out X           ≈⟨ pullˡ ∘[] ⟩
        [ (idC +₁ (F-Coalgebra-Morphism.f (Terminal.! (algebras X) {A = alg (now X)}))) ∘ i₁ 
        , (idC +₁ (F-Coalgebra-Morphism.f (Terminal.! (algebras X) {A = alg (now X)}))) ∘ i₂ ∘ i₁ ] ∘ out X                ≈⟨ ([]-cong₂ +₁∘i₁ (pullˡ +₁∘i₂)) ⟩∘⟨refl ⟩
        [ i₁ ∘ idC , (i₂ ∘ (F-Coalgebra-Morphism.f (Terminal.! (algebras X) {A = alg (now X)}))) ∘ i₁ ] ∘ out X            ≈⟨ ([]-cong₂ refl assoc) ⟩∘⟨refl ⟩
        [ i₁ ∘ idC , i₂ ∘ (extend (now X)) ] ∘ out X                                                                       ≈˘⟨ []∘+₁ ⟩∘⟨refl ⟩
        ([ i₁ , i₂ ] ∘ (idC +₁ extend (now X))) ∘ out X                                                                    ≈⟨ (elimˡ +-η) ⟩∘⟨refl ⟩
        (idC +₁ extend (now X)) ∘ out X                                                                                    ∎ })
      ; assoc = {!   !}
      ; sym-assoc = {!   !}
      ; extend-≈ = λ {X} {Y} {f} {g} eq → {!   !}
      
        -- begin 
        --   extend f ≈⟨ sym (Terminal.!-unique (algebras Y) (record { f = extend f ; commutes = F-Coalgebra-Morphism.commutes {!   !} })) ⟩ 
        --   F-Coalgebra-Morphism.f ((Terminal.! (algebras Y) {A = alg' {X} {Y}})) ≈˘⟨ sym (Terminal.!-unique (algebras Y) (record { f = extend g ; commutes = {!   !} })) ⟩
        --   extend g ∎
      
        -- let 
        --   h : F-Coalgebra-Morphism (alg f) (alg g)
        --   h = record { f = idC ; commutes = begin 
        --     F-Coalgebra.α (alg g) ∘ idC ≈⟨ id-comm ⟩ 
        --     idC ∘ F-Coalgebra.α (alg g) ≈⟨ refl⟩∘⟨ []-cong₂ (([]-cong₂ (refl⟩∘⟨ (refl⟩∘⟨ (sym eq))) refl) ⟩∘⟨refl) refl ⟩ 
        --     idC ∘ F-Coalgebra.α (alg f) ≈˘⟨ ([]-cong₂ identityʳ identityʳ ○ +-η) ⟩∘⟨refl ⟩
        --     (idC +₁ idC) ∘ F-Coalgebra.α (alg f) ∎ }
        --   x : F-Coalgebra-Morphism (alg f) (Terminal.⊤ (algebras Y))
        --   x = (F-Coalgebras (delayF Y)) [ Terminal.! (algebras Y) ∘ h ]
        -- in Terminal.!-unique₂ (algebras Y) {f = Terminal.! (algebras Y)} {g = {!   !} } ⟩∘⟨refl
        
        -- extend f ≈⟨ insertˡ (_≅_.isoˡ (out-≅ Y)) ⟩ 
        -- out⁻¹ Y ∘ out Y ∘ extend f ≈⟨ refl⟩∘⟨ pullˡ (F-Coalgebra-Morphism.commutes (Terminal.! (algebras Y) {A = alg f})) ⟩
        -- out⁻¹ Y ∘ ((idC +₁ (F-Coalgebra-Morphism.f (Terminal.! (algebras Y)))) ∘ [ [ [ i₁ , i₂ ∘ i₂ ] ∘ (out Y ∘ f) , i₂ ∘ i₁ ] ∘ out X , (idC +₁ i₂) ∘ out Y ]) ∘ i₁ ≈⟨ refl⟩∘⟨ ((+₁-cong₂ refl (Terminal.!-unique₂ (algebras Y) {f = Terminal.! (algebras Y) {A = alg f}} {g = Terminal.! (algebras Y) {A = alg f}}) ⟩∘⟨ ([]-cong₂ (([]-cong₂ (refl⟩∘⟨ (refl⟩∘⟨ eq)) refl) ⟩∘⟨refl) refl)) ⟩∘⟨refl) ⟩
        -- out⁻¹ Y ∘ ((idC +₁ (F-Coalgebra-Morphism.f (Terminal.! (algebras Y)))) ∘ [ [ [ i₁ , i₂ ∘ i₂ ] ∘ (out Y ∘ g) , i₂ ∘ i₁ ] ∘ out X , (idC +₁ i₂) ∘ out Y ]) ∘ i₁ ≈⟨ refl⟩∘⟨ (((+₁-cong₂ refl (Terminal.!-unique₂ (algebras Y) {f = Terminal.! (algebras Y)} {g = record { f = F-Coalgebra-Morphism.f (Terminal.! (algebras Y)) ; commutes = {!   !} }})) ⟩∘⟨refl) ⟩∘⟨refl) ⟩
        -- out⁻¹ Y ∘ ((idC +₁ (F-Coalgebra-Morphism.f (Terminal.! (algebras Y)))) ∘ [ [ [ i₁ , i₂ ∘ i₂ ] ∘ (out Y ∘ g) , i₂ ∘ i₁ ] ∘ out X , (idC +₁ i₂) ∘ out Y ]) ∘ i₁ ≈˘⟨ refl⟩∘⟨ pullˡ (F-Coalgebra-Morphism.commutes (Terminal.! (algebras Y) {A = alg g})) ⟩
        -- out⁻¹ Y ∘ out Y ∘ extend g ≈˘⟨ insertˡ (_≅_.isoˡ (out-≅ Y)) ⟩
        -- extend g ∎
      })
      where
        alg' : ∀ {X Y} → F-Coalgebra (delayF Y)
        alg' {X} {Y} = record { A = D₀ X ; α = i₂ }
        module _ {X Y : Obj} (f : X ⇒ D₀ Y) where
          open Terminal (algebras Y) using (!; ⊤-id)
          alg : F-Coalgebra (delayF Y)
          alg = record { A = D₀ X + D₀ Y ; α = [ [ [ i₁ , i₂ ∘ i₂ ] ∘ (out Y ∘ f) , i₂ ∘ i₁ ] ∘ out X , (idC +₁ i₂) ∘ out Y ] }  -- (idC +₁ (idC +₁ [ idC , idC ]) ∘ _≅_.to +-assoc ∘ _≅_.to +-comm)
          extend : D₀ X ⇒ D₀ Y
          extend = F-Coalgebra-Morphism.f (! {A = alg}) ∘ i₁ {B = D₀ Y}
          !∘i₂ : F-Coalgebra-Morphism.f (! {A = alg}) ∘ i₂ ≈ idC
          !∘i₂ = ⊤-id (F-Coalgebras (delayF Y) [ ! ∘ record { f = i₂ ; commutes = inject₂ } ] )
          extendlaw : out Y ∘ extend ≈ [ out Y ∘ f , i₂ ∘ extend ] ∘ out X
          extendlaw = begin 
            out Y ∘ extend ≈⟨ pullˡ (F-Coalgebra-Morphism.commutes (! {A = alg})) ⟩ 
            ((idC +₁ (F-Coalgebra-Morphism.f !)) ∘ F-Coalgebra.α alg) ∘ coproduct.i₁                   ≈⟨ pullʳ inject₁ ⟩
            (idC +₁ (F-Coalgebra-Morphism.f !)) ∘ [ [ i₁ , i₂ ∘ i₂ ] ∘ (out Y ∘ f) , i₂ ∘ i₁ ] ∘ out X ≈⟨ pullˡ ∘[] ⟩
            [ (idC +₁ (F-Coalgebra-Morphism.f !)) ∘ [ i₁ , i₂ ∘ i₂ ] ∘ (out Y ∘ f) 
            , (idC +₁ (F-Coalgebra-Morphism.f !)) ∘ i₂ ∘ i₁ ] ∘ out X                                  ≈⟨ ([]-cong₂ (pullˡ ∘[]) (pullˡ +₁∘i₂)) ⟩∘⟨refl ⟩
            [ [ (idC +₁ (F-Coalgebra-Morphism.f !)) ∘ i₁ 
              , (idC +₁ (F-Coalgebra-Morphism.f !)) ∘ i₂ ∘ i₂ ] ∘ (out Y ∘ f) 
            , (i₂ ∘ (F-Coalgebra-Morphism.f !)) ∘ i₁ ] ∘ out X                                         ≈⟨ ([]-cong₂ (([]-cong₂ +₁∘i₁ (pullˡ +₁∘i₂)) ⟩∘⟨refl) refl) ⟩∘⟨refl ⟩
            [ [ i₁ ∘ idC , (i₂ ∘ (F-Coalgebra-Morphism.f !)) ∘ i₂ ] ∘ (out Y ∘ f) 
            , (i₂ ∘ (F-Coalgebra-Morphism.f !)) ∘ i₁ ] ∘ out X                                         ≈⟨ ([]-cong₂ (elimˡ (([]-cong₂ identityʳ (cancelʳ !∘i₂)) ○ +-η)) assoc) ⟩∘⟨refl ⟩
            [ out Y ∘ f , i₂ ∘ extend ] ∘ out X ∎ 
```

### Old definitions:

```agda
  record DelayMonad : Set (o ⊔ ℓ ⊔ e) where
    field
      D₀ : Obj → Obj

    field
      now : ∀ {X} → X ⇒ D₀ X
      later : ∀ {X} → D₀ X ⇒ D₀ X
      isIso : ∀ {X} → IsIso ([ now {X} , later {X} ])

    out : ∀ {X} → D₀ X ⇒ X + D₀ X
    out {X} = IsIso.inv (isIso {X})

    field
      coit : ∀ {X Y} → Y ⇒ X + Y → Y ⇒ D₀ X
      coit-law : ∀ {X Y} {f : Y ⇒ X + Y} → out ∘ (coit f) ≈ (idC +₁ (coit f)) ∘ f

    field
      _* : ∀ {X Y} → X ⇒ D₀ Y → D₀ X ⇒ D₀ Y
      *-law : ∀ {X Y} {f : X ⇒ D₀ Y} → out ∘ (f *) ≈ [ out ∘ f , i₂ ∘ (f *) ] ∘ out
      *-unique : ∀ {X Y} (f : X ⇒ D₀ Y) (h : D₀ X ⇒ D₀ Y) → h ≈ f *
      *-resp-≈ : ∀ {X Y} {f h : X ⇒ D₀ Y} → f ≈ h → f * ≈ h * 

    unitLaw : ∀ {X} → out {X} ∘ now {X} ≈ i₁
    unitLaw = begin 
      out ∘ now                  ≈⟨ refl⟩∘⟨ sym inject₁ ⟩ 
      out ∘ [ now , later ] ∘ i₁ ≈⟨ cancelˡ (IsIso.isoˡ isIso) ⟩
      i₁ ∎

    toMonad : KleisliTriple C
    toMonad = record
      { F₀ = D₀
      ; unit = now
      ; extend = _*
      ; identityʳ = λ {X} {Y} {k} → begin 
        k * ∘ now                                                ≈⟨ introˡ (IsIso.isoʳ isIso) ⟩∘⟨refl ⟩ 
        (([ now , later ] ∘ out) ∘ k *) ∘ now                    ≈⟨ pullʳ *-law ⟩∘⟨refl ⟩
        ([ now , later ] ∘ [ out ∘ k , i₂ ∘ (k *) ] ∘ out) ∘ now ≈⟨ pullʳ (pullʳ unitLaw) ⟩
        [ now , later ] ∘ [ out ∘ k , i₂ ∘ (k *) ] ∘ i₁          ≈⟨ refl⟩∘⟨ inject₁ ⟩
        [ now , later ] ∘ out ∘ k                                ≈⟨ cancelˡ (IsIso.isoʳ isIso) ⟩
        k ∎
      ; identityˡ = λ {X} → sym (*-unique now idC)
      ; assoc = λ {X} {Y} {Z} {f} {g} → sym (*-unique ((g *) ∘ f) ((g *) ∘ (f *)))
      ; sym-assoc = λ {X} {Y} {Z} {f} {g} → *-unique ((g *) ∘ f) ((g *) ∘ (f *))
      ; extend-≈ = *-resp-≈
      }
```

### Definition 30: Search-Algebras

TODO

### Proposition 31 : the category of uniform-iteration algebras coincides with the category of search-algebras

TODO