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

24 KiB
Raw Blame History

Summary

This file introduces the delay monad D

  • Proposition 1 Characterization of the delay monad D
  • Proposition 2 D is commutative

Code

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

  CC : CartesianCategory o  e
  CC = record { U = C ; cartesian = (ExtensiveDistributiveCategory.cartesian ED) }

  open import Categories.Object.NaturalNumbers.Parametrized CC
  open import Categories.Object.NaturalNumbers.Properties.F-Algebras using (PNNO⇒Initial₂; PNNO-Algebra)

  open M C
  open MR C
  open Equiv
  open HomReasoning
  open CoLambek
  open F-Coalgebra-Morphism

Proposition 1: Characterization of the delay monad D

  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 (; !; !-unique)
      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 }})

      module _ ( : ParametrizedNNO) where
        open ParametrizedNNO 
      
        iso : X × N  X + X × N
        iso = Lambek.lambek (record {  = PNNO-Algebra CC coproducts X N z s ; ⊥-is-initial = PNNO⇒Initial₂ CC coproducts  X })

        ι : X × N  DX
        ι = f (! {A = record { A = X × N ; α = _≅_.from iso }})

        
    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 = λ {X} {Y} {Z} {g} {h}  {!   !}
      
      -- begin 
      --   extend (extend h ∘ g) ≈⟨ insertˡ (_≅_.isoˡ (out-≅ Z)) ⟩ 
      --   out⁻¹ Z ∘ out Z ∘ extend (extend h ∘ g) ≈⟨ refl⟩∘⟨ (pullˡ (commutes (! (algebras Z)))) ⟩ 
      --   out⁻¹ Z ∘ ((idC +₁ (f (! (algebras Z)))) ∘ F-Coalgebra.α (alg (extend h ∘ g))) ∘ i₁ ≈⟨ refl⟩∘⟨ (pullʳ inject₁) ⟩ 
      --   out⁻¹ Z ∘ (idC +₁ (f (! (algebras Z)))) ∘ [ [ i₁ , i₂ ∘ i₂ ] ∘ out Z ∘ extend h ∘ g , i₂ ∘ i₁ ] ∘ out X ≈⟨ refl⟩∘⟨ pullˡ ∘[] ⟩
      --   out⁻¹ Z ∘ [ (idC +₁ (f (! (algebras Z)))) ∘ [ i₁ , i₂ ∘ i₂ ] ∘ out Z ∘ extend h ∘ g , (idC +₁ (f (! (algebras Z)))) ∘ i₂ ∘ i₁ ] ∘ out X ≈⟨ refl⟩∘⟨ (([]-cong₂ (pullˡ ∘[]) (pullˡ +₁∘i₂)) ⟩∘⟨refl) ⟩
      --   out⁻¹ Z ∘ [ [ (idC +₁ (f (! (algebras Z)))) ∘ i₁ , (idC +₁ (f (! (algebras Z)))) ∘ i₂ ∘ i₂ ] ∘ out Z ∘ extend h ∘ g , (i₂ ∘ (f (! (algebras Z)))) ∘ i₁ ] ∘ out X ≈⟨ refl⟩∘⟨ (([]-cong₂ (([]-cong₂ (+₁∘i₁ ○ identityʳ) (pullˡ +₁∘i₂)) ⟩∘⟨refl) refl) ⟩∘⟨refl) ⟩
      --   out⁻¹ Z ∘ [ [ i₁ , (i₂ ∘ (f (! (algebras Z)))) ∘ i₂ ] ∘ out Z ∘ extend h ∘ g 
      --             , (i₂ ∘ (f (! (algebras Z)))) ∘ i₁ 
      --             ] ∘ out X ≈⟨ refl⟩∘⟨ (([]-cong₂ (refl⟩∘⟨ (pullˡ (pullˡ (commutes (! (algebras Z)))))) refl) ⟩∘⟨refl) ⟩
      --   out⁻¹ Z ∘ [ [ i₁ , (i₂ ∘ (f (! (algebras Z)))) ∘ i₂ ] ∘ (((idC +₁ f (! (algebras Z))) ∘ F-Coalgebra.α (alg h)) ∘ i₁) ∘ g , (i₂ ∘ (f (! (algebras Z)))) ∘ i₁ ] ∘ out X ≈⟨ refl⟩∘⟨ (([]-cong₂ (refl⟩∘⟨ ((pullʳ inject₁) ⟩∘⟨refl)) refl) ⟩∘⟨refl) ⟩
      --   out⁻¹ Z ∘ [ [ i₁ , (i₂ ∘ (f (! (algebras Z)))) ∘ i₂ ] ∘ ((idC +₁ f (! (algebras Z))) ∘ [ [ i₁ , i₂ ∘ i₂ ] ∘ out Z ∘ h , i₂ ∘ i₁ ] ∘ out Y) ∘ g , (i₂ ∘ (f (! (algebras Z)))) ∘ i₁ ] ∘ out X ≈⟨ refl⟩∘⟨ (([]-cong₂ (pullˡ (pullˡ []∘+₁)) refl) ⟩∘⟨refl) ⟩
      --   out⁻¹ Z ∘ [ ([ i₁ ∘ idC , ((i₂ ∘ (f (! (algebras Z)))) ∘ i₂) ∘ f (! (algebras Z)) ] ∘ ([ [ i₁ , i₂ ∘ i₂ ] ∘ out Z ∘ h , i₂ ∘ i₁ ] ∘ out Y)) ∘ g , (i₂ ∘ (f (! (algebras Z)))) ∘ i₁ ] ∘ out X ≈⟨ refl⟩∘⟨ (([]-cong₂ ((pullˡ ∘[]) ⟩∘⟨refl) refl) ⟩∘⟨refl) ⟩
      --   out⁻¹ Z ∘ [ ([ [ i₁ ∘ idC , ((i₂ ∘ (f (! (algebras Z)))) ∘ i₂) ∘ f (! (algebras Z)) ] ∘ [ i₁ , i₂ ∘ i₂ ] ∘ out Z ∘ h , [ i₁ ∘ idC , ((i₂ ∘ (f (! (algebras Z)))) ∘ i₂) ∘ f (! (algebras Z)) ] ∘ i₂ ∘ i₁ ] ∘ out Y) ∘ g , (i₂ ∘ (f (! (algebras Z)))) ∘ i₁ ] ∘ out X ≈⟨ refl⟩∘⟨ (([]-cong₂ ((([]-cong₂ (pullˡ ∘[]) (pullˡ inject₂)) ⟩∘⟨refl) ⟩∘⟨refl) refl) ⟩∘⟨refl) ⟩ 
      --   out⁻¹ Z ∘ [ ([ [ [ i₁ ∘ idC , ((i₂ ∘ (f (! (algebras Z)))) ∘ i₂) ∘ f (! (algebras Z)) ] ∘ i₁ , [ i₁ ∘ idC , ((i₂ ∘ (f (! (algebras Z)))) ∘ i₂) ∘ f (! (algebras Z)) ] ∘ i₂ ∘ i₂ ] ∘ out Z ∘ h , (((i₂ ∘ (f (! (algebras Z)))) ∘ i₂) ∘ f (! (algebras Z))) ∘ i₁ ] ∘ out Y) ∘ g , (i₂ ∘ (f (! (algebras Z)))) ∘ i₁ ] ∘ out X ≈⟨ refl⟩∘⟨ (([]-cong₂ ((([]-cong₂ (([]-cong₂ inject₁ (pullˡ inject₂)) ⟩∘⟨refl) refl) ⟩∘⟨refl) ⟩∘⟨refl) refl) ⟩∘⟨refl) ⟩ 
      --   out⁻¹ Z ∘ [ ([ [ i₁ ∘ idC , (((i₂ ∘ (f (! (algebras Z)))) ∘ i₂) ∘ f (! (algebras Z))) ∘ i₂ ] ∘ out Z ∘ h , (((i₂ ∘ (f (! (algebras Z)))) ∘ i₂) ∘ f (! (algebras Z))) ∘ i₁ ] ∘ out Y) ∘ g 
      --             , (i₂ ∘ (f (! (algebras Z)))) ∘ i₁ 
      --             ] ∘ out X ≈⟨ {!   !} ⟩ 
      --   {!   !} ≈⟨ {!   !} ⟩ 
      --   {!   !} ≈˘⟨ {!  _○_ !} ⟩ 
      --   {!   !} ≈˘⟨ {!   !} ⟩ 
      --   {!   !} ≈˘⟨ {!   !} ⟩ 
      --   out⁻¹ Z ∘ [ [ [ i₁ , (i₂ ∘ f (! (algebras Z))) ∘ i₂ ] ∘ out Z ∘ h , (((i₂ ∘ f (! (algebras Z))) ∘ i₁) ∘ f (! (algebras Y))) ∘ i₂ ] ∘ out Y ∘ g 
      --             , (((i₂ ∘ f (! (algebras Z))) ∘ i₁) ∘ f (! (algebras Y))) ∘ i₁ 
      --             ] ∘ out X ≈˘⟨ refl⟩∘⟨ (([]-cong₂ (([]-cong₂ inject₁ (pullˡ inject₂)) ⟩∘⟨refl) refl) ⟩∘⟨refl) ⟩ 
      --   out⁻¹ Z ∘ [ [ [ [ i₁ , (i₂ ∘ f (! (algebras Z))) ∘ i₂ ] ∘ out Z ∘ h , ((i₂ ∘ f (! (algebras Z))) ∘ i₁) ∘ f (! (algebras Y)) ] ∘ i₁ , [ [ i₁ , (i₂ ∘ f (! (algebras Z))) ∘ i₂ ] ∘ out Z ∘ h , ((i₂ ∘ f (! (algebras Z))) ∘ i₁) ∘ f (! (algebras Y)) ] ∘ i₂ ∘ i₂ ] ∘ out Y ∘ g 
      --             , (((i₂ ∘ f (! (algebras Z))) ∘ i₁) ∘ f (! (algebras Y))) ∘ i₁ ] ∘ out X ≈˘⟨ refl⟩∘⟨ (([]-cong₂ (pullˡ ∘[]) (pullˡ inject₂)) ⟩∘⟨refl) ⟩ 
      --   out⁻¹ Z ∘ [ [ [ i₁ , (i₂ ∘ f (! (algebras Z))) ∘ i₂ ] ∘ out Z ∘ h , ((i₂ ∘ f (! (algebras Z))) ∘ i₁) ∘ f (! (algebras Y)) ] ∘ [ i₁ , i₂ ∘ i₂ ] ∘ out Y ∘ g 
      --             , [ [ i₁ , (i₂ ∘ f (! (algebras Z))) ∘ i₂ ] ∘ out Z ∘ h , ((i₂ ∘ f (! (algebras Z))) ∘ i₁) ∘ f (! (algebras Y)) ] ∘ i₂ ∘ i₁ ] ∘ out X ≈˘⟨ refl⟩∘⟨ (pullˡ ∘[]) ⟩ 
      --   out⁻¹ Z ∘ [ [ i₁ , (i₂ ∘ f (! (algebras Z))) ∘ i₂ ] ∘ out Z ∘ h , ((i₂ ∘ f (! (algebras Z))) ∘ i₁) ∘ f (! (algebras Y)) ] ∘ [ [ i₁ , i₂ ∘ i₂ ] ∘ out Y ∘ g , i₂ ∘ i₁ ] ∘ out X ≈˘⟨ refl⟩∘⟨ (([]-cong₂ (([]-cong₂ (+₁∘i₁ ○ identityʳ) (pullˡ +₁∘i₂)) ⟩∘⟨refl) refl) ⟩∘⟨refl) ⟩ 
      --   out⁻¹ Z ∘ [ [ (idC +₁ f (! (algebras Z))) ∘ i₁ , (idC +₁ f (! (algebras Z))) ∘ i₂ ∘ i₂ ] ∘ out Z ∘ h , ((i₂ ∘ f (! (algebras Z))) ∘ i₁) ∘ f (! (algebras Y)) ] ∘ [ [ i₁ , i₂ ∘ i₂ ] ∘ out Y ∘ g , i₂ ∘ i₁ ] ∘ out X ≈˘⟨ refl⟩∘⟨ (([]-cong₂ ((refl⟩∘⟨ identityʳ) ○ (pullˡ ∘[])) (pullˡ (pullˡ +₁∘i₂))) ⟩∘⟨refl) ⟩ 
      --   out⁻¹ Z ∘ [ (idC +₁ f (! (algebras Z))) ∘ ([ i₁ , i₂ ∘ i₂ ] ∘ out Z ∘ h) ∘ idC , (idC +₁ f (! (algebras Z))) ∘ (i₂ ∘ i₁) ∘ f (! (algebras Y)) ] ∘ [ [ i₁ , i₂ ∘ i₂ ] ∘ out Y ∘ g , i₂ ∘ i₁ ] ∘ out X ≈˘⟨ refl⟩∘⟨ (pullˡ ∘[]) ⟩ 
      --   out⁻¹ Z ∘ (idC +₁ f (! (algebras Z))) ∘ [ ([ i₁ , i₂ ∘ i₂ ] ∘ out Z ∘ h) ∘ idC , (i₂ ∘ i₁) ∘ f (! (algebras Y)) ] ∘ [ [ i₁ , i₂ ∘ i₂ ] ∘ out Y ∘ g , i₂ ∘ i₁ ] ∘ out X ≈˘⟨ refl⟩∘⟨ (refl⟩∘⟨ (pullˡ []∘+₁)) ⟩ 
      --   out⁻¹ Z ∘ (idC +₁ f (! (algebras Z))) ∘ [ [ i₁ , i₂ ∘ i₂ ] ∘ out Z ∘ h , i₂ ∘ i₁ ] 
      --   ∘ (idC +₁ f (! (algebras Y))) ∘ [ [ i₁ , i₂ ∘ i₂ ] ∘ out Y ∘ g , i₂ ∘ i₁ ] ∘ out X ≈˘⟨ refl⟩∘⟨ (refl⟩∘⟨ (refl⟩∘⟨ identityˡ)) ⟩ 
      --   out⁻¹ Z ∘ (idC +₁ f (! (algebras Z))) ∘ [ [ i₁ , i₂ ∘ i₂ ] ∘ out Z ∘ h , i₂ ∘ i₁ ] ∘ idC 
      --   ∘ (idC +₁ f (! (algebras Y))) ∘ [ [ i₁ , i₂ ∘ i₂ ] ∘ out Y ∘ g , i₂ ∘ i₁ ] ∘ out X ≈˘⟨ pullʳ (pullʳ (pullʳ (pullˡ (_≅_.isoʳ (out-≅ Y))))) ⟩ 
      --   (out⁻¹ Z ∘ (idC +₁ f (! (algebras Z))) ∘ [ [ i₁ , i₂ ∘ i₂ ] ∘ out Z ∘ h , i₂ ∘ i₁ ] ∘ out Y) 
      --   ∘ (out⁻¹ Y ∘ (idC +₁ f (! (algebras Y))) ∘ [ [ i₁ , i₂ ∘ i₂ ] ∘ out Y ∘ g , i₂ ∘ i₁ ] ∘ out X) ≈˘⟨ (refl⟩∘⟨ (pullʳ inject₁)) ⟩∘⟨ (refl⟩∘⟨ (pullʳ inject₁)) ⟩ 
      --   (out⁻¹ Z ∘ ((idC +₁ (f (! (algebras Z)))) ∘ F-Coalgebra.α (alg h)) ∘ i₁) ∘ (out⁻¹ Y ∘ ((idC +₁ (f (! (algebras Y)))) ∘ F-Coalgebra.α (alg g)) ∘ i₁) ≈˘⟨ (refl⟩∘⟨ (pullˡ (commutes (! (algebras Z))))) ⟩∘⟨ refl⟩∘⟨ (pullˡ (commutes (! (algebras Y)))) ⟩ 
      --   (out⁻¹ Z ∘ out Z ∘ extend h) ∘ (out⁻¹ Y ∘ out Y ∘ extend g) ≈˘⟨ ((insertˡ (_≅_.isoˡ (out-≅ Z)))) ⟩∘⟨ ((insertˡ (_≅_.isoˡ (out-≅ Y)))) ⟩ 
      --   extend h ∘ extend g ∎


        -- begin 
        -- extend (extend h ∘ g) ≈⟨ (insertˡ (_≅_.isoˡ (out-≅ Z))) ⟩ 
        -- out⁻¹ Z ∘ out Z ∘ extend (extend h ∘ g) ≈⟨ refl⟩∘⟨ extendlaw (extend h ∘ g) ⟩ 
        -- out⁻¹ Z ∘ [ out Z ∘ extend h ∘ g , i₂ ∘ extend (extend h ∘ g) ] ∘ out X ≈⟨ {!   !} ⟩ 
        -- {!   !} ≈⟨ {!   !} ⟩ 
        -- {!   !} ≈⟨ {!   !} ⟩ 
        -- {!   !} ≈⟨ {!   !} ⟩ 
        -- {!   !} ≈˘⟨ {!   !} ⟩ 
        -- {!   !} ≈˘⟨ {!   !} ⟩ 
        -- out⁻¹ Z ∘ [ [ out Z ∘ h , i₂ ∘ extend h ] ∘ out Y ∘ g , (i₂ ∘ extend h) ∘ extend g ] ∘ out X ≈˘⟨ refl⟩∘⟨ (([]-cong₂ refl (pullˡ inject₂)) ⟩∘⟨refl) ⟩ 
        -- out⁻¹ Z ∘ [ [ out Z ∘ h , i₂ ∘ extend h ] ∘ out Y ∘ g , [ out Z ∘ h , i₂ ∘ extend h ] ∘ i₂ ∘ extend g ] ∘ out X ≈˘⟨ refl⟩∘⟨ (pullˡ ∘[]) ⟩ 
        -- out⁻¹ Z ∘ [ out Z ∘ h , i₂ ∘ extend h ] ∘ [ out Y ∘ g , i₂ ∘ extend g ] ∘ out X ≈˘⟨ refl⟩∘⟨ (refl⟩∘⟨ identityˡ) ⟩ 
        -- out⁻¹ Z ∘ [ out Z ∘ h , i₂ ∘ extend h ] ∘ idC ∘ [ out Y ∘ g , i₂ ∘ extend g ] ∘ out X ≈˘⟨ pullʳ (pullʳ (pullˡ (_≅_.isoʳ (out-≅ Y)))) ⟩ 
        -- (out⁻¹ Z ∘ [ out Z ∘ h , i₂ ∘ extend h ] ∘ out Y) ∘ out⁻¹ Y ∘ [ out Y ∘ g , i₂ ∘ extend g ] ∘ out X ≈˘⟨ (refl⟩∘⟨ extendlaw h) ⟩∘⟨ (refl⟩∘⟨ extendlaw g) ⟩ 
        -- (out⁻¹ Z ∘ out Z ∘ extend h) ∘ (out⁻¹ Y ∘ out Y ∘ extend g) ≈˘⟨ ((insertˡ (_≅_.isoˡ (out-≅ Z)))) ⟩∘⟨ ((insertˡ (_≅_.isoˡ (out-≅ Y)))) ⟩ 
        -- extend h ∘ extend g ∎


        --begin 
        -- f (! (algebras Z) {A = alg (extend h ∘ g)}) ∘ i₁ {A = D₀ X} {B = D₀ Z} ≈⟨ (!-unique (algebras Z) (record { f = {! (f (! (algebras Z) {A = alg h}) ∘ i₁) ∘ f (! (algebras Y) {A = alg g})  !} ; commutes = {!   !} })) ⟩∘⟨refl ⟩ 
        -- {!   !} ∘ i₁ ≈⟨ {!   !} ⟩
        -- (f (! (algebras Z) {A = alg h}) ∘ i₁) ∘ f (! (algebras Y) {A = alg g}) ∘ i₁ ∎
      ; sym-assoc = λ {X} {Y} {Z} {g} {h}  {!   !}
      ; extend-≈ = λ {X} {Y} {f} {g} eq  begin 
          F-Coalgebra-Morphism.f (Terminal.! (algebras Y) {A = alg f })  i₁ {B = D₀ Y} ≈⟨ (Terminal.!-unique (algebras Y) (record { f = (F-Coalgebra-Morphism.f (Terminal.! (algebras Y) {A = alg g })  idC) ; commutes = begin 
            F-Coalgebra.α (Terminal. (algebras Y))  F-Coalgebra-Morphism.f (Terminal.! (algebras Y))  idC ≈⟨ refl⟩∘⟨ identityʳ  
            F-Coalgebra.α (Terminal. (algebras Y))  F-Coalgebra-Morphism.f (Terminal.! (algebras Y)) ≈⟨ F-Coalgebra-Morphism.commutes (Terminal.! (algebras Y))  
            Functor.F₁ (delayF Y) (F-Coalgebra-Morphism.f (Terminal.! (algebras Y)))  F-Coalgebra.α (alg g) ≈˘⟨ (Functor.F-resp-≈ (delayF Y) identityʳ) ⟩∘⟨ (αf≈αg eq)  
            Functor.F₁ (delayF Y) (F-Coalgebra-Morphism.f (Terminal.! (algebras Y))  idC)  F-Coalgebra.α (alg f)  })) ⟩∘⟨refl  
          (F-Coalgebra-Morphism.f (Terminal.! (algebras Y) {A = alg g })  idC)  i₁ {B = D₀ Y} ≈⟨ identityʳ ⟩∘⟨refl 
          extend g 
      })
      where
        open Terminal
        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 (! (algebras Y) {A = alg})  i₁ {B = D₀ Y}
          !∘i₂ : F-Coalgebra-Morphism.f (! (algebras Y) {A = alg})  i₂  idC
          !∘i₂ = -id (algebras Y) (F-Coalgebras (delayF Y) [ ! (algebras 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 (! (algebras Y) {A = alg}))  
            ((idC +₁ (F-Coalgebra-Morphism.f (! (algebras Y))))  F-Coalgebra.α alg)  coproduct.i₁                   ≈⟨ pullʳ inject₁ 
            (idC +₁ (F-Coalgebra-Morphism.f (! (algebras Y))))  [ [ i₁ , i₂  i₂ ]  (out Y  f) , i₂  i₁ ]  out X ≈⟨ pullˡ ∘[] 
            [ (idC +₁ (F-Coalgebra-Morphism.f (! (algebras Y))))  [ i₁ , i₂  i₂ ]  (out Y  f) 
            , (idC +₁ (F-Coalgebra-Morphism.f (! (algebras Y))))  i₂  i₁ ]  out X                                  ≈⟨ ([]-cong₂ (pullˡ ∘[]) (pullˡ +₁∘i₂)) ⟩∘⟨refl 
            [ [ (idC +₁ (F-Coalgebra-Morphism.f (! (algebras Y))))  i₁ 
              , (idC +₁ (F-Coalgebra-Morphism.f (! (algebras Y))))  i₂  i₂ ]  (out Y  f) 
            , (i₂  (F-Coalgebra-Morphism.f (! (algebras Y))))  i₁ ]  out X                                         ≈⟨ ([]-cong₂ (([]-cong₂ +₁∘i₁ (pullˡ +₁∘i₂)) ⟩∘⟨refl) refl) ⟩∘⟨refl 
            [ [ i₁  idC , (i₂  (F-Coalgebra-Morphism.f (! (algebras Y))))  i₂ ]  (out Y  f) 
            , (i₂  (F-Coalgebra-Morphism.f (! (algebras Y))))  i₁ ]  out X                                         ≈⟨ ([]-cong₂ (elimˡ (([]-cong₂ identityʳ (cancelʳ !∘i₂))  +-η)) assoc) ⟩∘⟨refl 
            [ out Y  f , i₂  extend ]  out X  
          extend-unique : (g : D₀ X  D₀ Y)  extend  g
          extend-unique g = {!   !}
            -- begin 
          --   F-Coalgebra-Morphism.f (! (algebras Y) {A = alg}) ∘ i₁ {B = D₀ Y} ≈⟨ (!-unique (algebras Y) (record { f = [ g , idC ] ; commutes = begin 
          --     out Y ∘ [ g , idC ] ≈⟨ ∘[] ⟩ 
          --     [ out Y ∘ g , out Y ∘ idC ] ≈⟨ []-cong₂ {!   !} identityʳ ⟩
          --     {!   !} ≈˘⟨ {!   !} ⟩
          --     [ ([ out Y , i₂ ] ∘ (f +₁ g)) ∘ out X , out Y ] ≈˘⟨ []-cong₂ (sym []∘+₁ ⟩∘⟨refl) refl ⟩
          --     [ [ out Y ∘ f , i₂ ∘ g ] ∘ out X , out Y ] ≈˘⟨ {!   !} ⟩
          --     [ [ [ i₁ , i₂ ∘ idC ] ∘ (out Y ∘ f) , i₂ ∘ g ] ∘ out X , out Y ] ≈˘⟨ []-cong₂ (([]-cong₂ (([]-cong₂ identityʳ (pullʳ inject₂)) ⟩∘⟨refl) refl) ⟩∘⟨refl) refl ⟩
          --     [ [ [ i₁ ∘ idC , (i₂ ∘ [ g , idC ]) ∘ i₂ ] ∘ (out Y ∘ f) , i₂ ∘ g ] ∘ out X , out Y ] ≈˘⟨ []-cong₂ (([]-cong₂ (([]-cong₂ +₁∘i₁ (pullˡ +₁∘i₂)) ⟩∘⟨refl) (pullʳ inject₁)) ⟩∘⟨refl) (elimˡ (Functor.identity (delayF Y))) ⟩
          --     [ [ [ (idC +₁ [ g , idC ]) ∘ i₁ , (idC +₁ [ g , idC ]) ∘ i₂ ∘ i₂ ] ∘ (out Y ∘ f) , (i₂ ∘ [ g , idC ]) ∘ i₁ ] ∘ out X , (idC +₁ idC) ∘ out Y ] ≈˘⟨ []-cong₂ (([]-cong₂ (pullˡ ∘[]) (pullˡ +₁∘i₂)) ⟩∘⟨refl) ((+₁-cong₂ identity² inject₂) ⟩∘⟨refl) ⟩
          --     [ [ (idC +₁ [ g , idC ]) ∘ [ i₁ , i₂ ∘ i₂ ] ∘ (out Y ∘ f) , (idC +₁ [ g , idC ]) ∘ i₂ ∘ i₁ ] ∘ out X , (idC ∘ idC +₁ [ g , idC ] ∘ i₂) ∘ out Y ] ≈˘⟨ []-cong₂ (pullˡ ∘[]) (pullˡ +₁∘+₁) ⟩
          --     [ (idC +₁ [ g , idC ]) ∘ [ [ i₁ , i₂ ∘ i₂ ] ∘ (out Y ∘ f) , i₂ ∘ i₁ ] ∘ out X , (idC +₁ [ g , idC ]) ∘ (idC +₁ i₂) ∘ out Y ] ≈˘⟨ ∘[] ⟩
          --     (idC +₁ [ g , idC ]) ∘ F-Coalgebra.α alg ∎ })) ⟩∘⟨refl ⟩ 
          --   [ g , idC ] ∘ i₁ ≈⟨ inject₁ ⟩
          --   g ∎
        αf≈αg :  {X Y} {f g : X  D₀ Y}  f  g  F-Coalgebra.α (alg f)  F-Coalgebra.α (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} eq = record 
          { from = record { f = idC ; commutes = begin 
            F-Coalgebra.α (alg g)  idC ≈⟨ identityʳ  
            F-Coalgebra.α (alg g) ≈⟨  (αf≈αg eq)  
            F-Coalgebra.α (alg f) ≈˘⟨ elimˡ (Functor.identity (delayF Y))  
            Functor.F₁ (delayF Y) idC  F-Coalgebra.α (alg f)  } 
          ; to = record { f = idC ; commutes = begin 
            F-Coalgebra.α (alg f)  idC ≈⟨ identityʳ  
            F-Coalgebra.α (alg f) ≈⟨ αf≈αg eq  
            F-Coalgebra.α (alg g) ≈˘⟨ elimˡ (Functor.identity (delayF Y))  
            Functor.F₁ (delayF Y) idC  F-Coalgebra.α (alg g)  } 
          ; iso = record 
            { isoˡ = identity² 
            ; isoʳ = identity² 
            } 
          }

Definition 30: Search-Algebras

TODO

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

TODO