open import Level
open import Categories.Category
open import Categories.Monad hiding (id)
open import Categories.Monad.Relative renaming (Monad to RMonad)
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 renaming (id to idF)
open import Categories.Functor.Algebra
open import Categories.Monad.Construction.Kleisli
open import Categories.Category.Construction.F-Coalgebras
open import Categories.NaturalTransformation hiding (id)
open import Data.Product using (∃-syntax; _,_; Σ-syntax)
open import Categories.Category.Cocartesian

import Categories.Morphism as M
import Categories.Morphism.Reasoning as MR
import Categories.Morphism.Properties as MP


module Monad.Instance.Delay {o ℓ e} {C : Category o ℓ e} (cocartesian : Cocartesian C) where
  open Cocartesian cocartesian renaming (+-unique to []-unique)
  open Category C
  open M C
  open MR C
  open MP C using (Iso⇒Mono; Iso⇒Epi; Iso-swap)
  open Equiv
  open HomReasoning
  open CoLambek
  open F-Coalgebra-Morphism renaming (f to u)
  open F-Coalgebra

  record DelayM : Set (o ⊔ ℓ ⊔ e) where
    field
      coalgebras : ∀ (A : Obj) → Terminal (F-Coalgebras (A +-))

    -- out, out⁻¹, now, later
    module _ {X : Obj} where
      open Terminal (coalgebras X) using (⊤; !; !-unique)
      open F-Coalgebra ⊤ using () renaming (A to DX)

      private
        out-≅ : DX ≅ X + DX
        out-≅ = colambek {F = X +- } (coalgebras X)

      abstract
        out : DX ⇒ X + DX
        out = _≅_.from out-≅

        out⁻¹ : X + DX ⇒ DX
        out⁻¹ = _≅_.to out-≅

        out∘out⁻¹ : out ∘ out⁻¹ ≈ id
        out∘out⁻¹ = _≅_.isoʳ out-≅

        out⁻¹∘out : out⁻¹ ∘ out ≈ id
        out⁻¹∘out = _≅_.isoˡ out-≅

        out-mono : Mono out
        out-mono = Iso⇒Mono (_≅_.iso out-≅)

        out-epi : Epi out
        out-epi = Iso⇒Epi (_≅_.iso out-≅)

        out⁻¹-mono : Mono out⁻¹
        out⁻¹-mono = Iso⇒Mono (Iso-swap (_≅_.iso out-≅))

        out⁻¹-epi : Epi out⁻¹
        out⁻¹-epi = Iso⇒Epi (Iso-swap (_≅_.iso out-≅))

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

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

      earlier : DX ⇒ DX
      earlier = [ now , id ] ∘ out

      earlier∘now : earlier ∘ now ≈ now
      earlier∘now = pullʳ (cancelˡ out∘out⁻¹) ○ inject₁

      earlier∘later : earlier ∘ later ≈ id
      earlier∘later = pullʳ (cancelˡ out∘out⁻¹) ○ inject₂

      out⁻¹-now-later : out⁻¹ ≈ [ now , later ]
      out⁻¹-now-later = begin 
        out⁻¹               ≈⟨ introʳ +-η ⟩ 
        out⁻¹ ∘ [ i₁ , i₂ ] ≈⟨ ∘[] ⟩ 
        [ now , later ]     ∎ 

      unitlaw : out ∘ now ≈ i₁
      unitlaw = cancelˡ out∘out⁻¹

      laterlaw : out ∘ later ≈ i₂
      laterlaw = cancelˡ out∘out⁻¹

      out∘earlier : out ∘ earlier ≈ [ i₁ , out ] ∘ out
      out∘earlier = begin
        out ∘ earlier                   ≈⟨ pullˡ ∘[] ⟩
        [ out ∘ now , out ∘ id ] ∘ out  ≈⟨ []-cong₂ unitlaw identityʳ ⟩∘⟨refl ⟩
        [ i₁ , out ] ∘ out              ∎

      D-jointly-epic : ∀ {Y} {f g : DX ⇒ Y} → (f ∘ now ≈ g ∘ now) → (f ∘ later ≈ g ∘ later) → f ≈ g
      D-jointly-epic {Y} {f} {g} eq-now eq-later = begin 
        f                             ≈⟨ introʳ out⁻¹∘out ⟩ 
        f ∘ out⁻¹ ∘ out               ≈⟨ pullˡ (∘-resp-≈ʳ out⁻¹-now-later ○ ∘[]) ⟩ 
        [ f ∘ now , f ∘ later ] ∘ out ≈⟨ ([]-cong₂ eq-now eq-later) ⟩∘⟨refl ⟩ 
        [ g ∘ now , g ∘ later ] ∘ out ≈˘⟨ pullˡ (∘-resp-≈ʳ out⁻¹-now-later ○ ∘[]) ⟩ 
        g ∘ out⁻¹ ∘ out               ≈⟨ elimʳ out⁻¹∘out ⟩ 
        g                             ∎

    -- make DX more accessible
    D₀ : Obj → Obj
    D₀ X = F-Coalgebra.A (Terminal.⊤ (coalgebras X))

    -- coℕ = D₀ ⊤

    -- coiteration
    module Coit {X : Obj} where 
      open Terminal (coalgebras X) using (!; !-unique)
      abstract
        coit : ∀ {Y} → Y ⇒ X + Y → Y ⇒ D₀ X
        coit {Y} f = u (! {A = record { A = Y ; α = f }})

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

        coit-unique : ∀ {Y} (f : Y ⇒ X + Y) (f' : Y ⇒ D₀ X) → out ∘ f' ≈ (id +₁ f') ∘ f → coit f ≈ f'
        coit-unique f f' eq = Terminal.!-unique (coalgebras X) (record { f = f' ; commutes = eq })

        coit-unique' : ∀ {Y} (f : Y ⇒ X + Y) (f' f'' : Y ⇒ D₀ X) → out ∘ f' ≈ (id +₁ f') ∘ f → out ∘ f'' ≈ (id +₁ f'') ∘ f → f' ≈ f''
        coit-unique' f f' f'' eq₁ eq₂ = sym (coit-unique f f' eq₁) ○ coit-unique f f'' eq₂

        coit-resp-≈ : ∀ {Y} {f g : Y ⇒ X + Y} → f ≈ g → coit f ≈ coit g
        coit-resp-≈ {Y} {f} {g} eq = Terminal.!-unique (coalgebras X) (record { f = coit g ; commutes = begin 
          out ∘ coit g       ≈⟨ coit-commutes g ⟩ 
          (id +₁ coit g) ∘ g ≈⟨ refl⟩∘⟨ sym eq ⟩ 
          (id +₁ coit g) ∘ f ∎ })

        coit-refl : coit out ≈ id {D₀ X}
        coit-refl = coit-unique out id (id-comm ○ ∘-resp-≈ˡ (sym ([]-unique id-comm-sym id-comm-sym)))

        coit-now : coit i₁ ≈ now
        coit-now = coit-unique i₁ now (unitlaw ○ sym (inject₁ ○ identityʳ))
    open Coit

    module P-Corec {X Y : Obj} where
      abstract
        private
          p-corec' : (Y ⇒ X + (Y + D₀ X)) → (Y ⇒ D₀ X)
          p-corec' f = coit ([ f , (id +₁ i₂) ∘ out ]) ∘ i₁ {Y} {D₀ X}
          p-corec-commutes' : ∀ (f : Y ⇒ X + (Y + D₀ X)) → out ∘ p-corec' f ≈ (id +₁ [ p-corec' f , id ]) ∘ f
          p-corec-commutes' f = begin 
            out ∘ coit ([ f , (id +₁ i₂) ∘ out ]) ∘ i₁                                                  ≈⟨ extendʳ (coit-commutes ([ f , (id +₁ i₂) ∘ out ])) ⟩ 
            (id +₁ coit ([ f , (id +₁ i₂) ∘ out ])) ∘ [ f , (id +₁ i₂) ∘ out ] ∘ i₁                     ≈⟨ refl⟩∘⟨ inject₁ ⟩ 
            (id +₁ coit ([ f , (id +₁ i₂) ∘ out ])) ∘ f                                                 ≈˘⟨ (+₁-cong₂ refl +-g-η) ⟩∘⟨refl ⟩ 
            (id +₁ [ coit ([ f , (id +₁ i₂) ∘ out ]) ∘ i₁ , coit ([ f , (id +₁ i₂) ∘ out ]) ∘ i₂ ]) ∘ f ≈⟨ (+₁-cong₂ refl ([]-cong₂ refl (sym helper ○ coit-refl))) ⟩∘⟨refl ⟩
            (id +₁ [ p-corec' f , id ]) ∘ f                                                             ∎
            where
            helper : coit out ≈ coit ([ f , (id +₁ i₂) ∘ out ]) ∘ i₂
            helper = coit-unique out (coit ([ f , (id +₁ i₂) ∘ out ]) ∘ i₂) (begin 
              out ∘ coit ([ f , (id +₁ i₂) ∘ out ]) ∘ i₂                              ≈⟨ extendʳ (coit-commutes ([ f , (id +₁ i₂) ∘ out ])) ⟩ 
              (id +₁ coit ([ f , (id +₁ i₂) ∘ out ])) ∘ [ f , (id +₁ i₂) ∘ out ] ∘ i₂ ≈⟨ refl⟩∘⟨ inject₂ ⟩ 
              (id +₁ coit ([ f , (id +₁ i₂) ∘ out ])) ∘ (id +₁ i₂) ∘ out              ≈⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ identity² refl) ⟩ 
              (id +₁ coit ([ f , (id +₁ i₂) ∘ out ]) ∘ i₂) ∘ out                      ∎)
          p-corec-unique' : ∀ (f : Y ⇒ X + (Y + D₀ X)) (g : Y ⇒ D₀ X) → out ∘ g ≈ (id +₁ [ g , id ]) ∘ f → p-corec' f ≈ g
          p-corec-unique' f g eq = begin 
            coit ([ f , (id +₁ i₂) ∘ out ]) ∘ i₁ ≈⟨ (coit-unique ([ f , (id +₁ i₂) ∘ out ]) [ g , id ] helper) ⟩∘⟨refl ⟩ 
            [ g , id ] ∘ i₁ ≈⟨ inject₁ ⟩ 
            g ∎
            where
            helper : out ∘ [ g , id ] ≈ (id +₁ [ g , id ]) ∘ [ f , (id +₁ i₂) ∘ out ]
            helper = begin 
              out ∘ [ g , id ]                                                   ≈⟨ ∘[] ⟩ 
              [ out ∘ g , out ∘ id ]                                             ≈⟨ []-cong₂ eq identityʳ ⟩ 
              [ (id +₁ [ g , id ]) ∘ f , out ]                                   ≈˘⟨ []-cong₂ refl (elimˡ ([]-unique id-comm-sym id-comm-sym)) ⟩ 
              [ (id +₁ [ g , id ]) ∘ f , (id +₁ id) ∘ out ]                      ≈˘⟨ []-cong₂ refl (pullˡ (+₁∘+₁ ○ +₁-cong₂ identity² inject₂)) ⟩ 
              [ (id +₁ [ g , id ]) ∘ f , (id +₁ [ g , id ]) ∘ (id +₁ i₂) ∘ out ] ≈˘⟨ ∘[] ⟩ 
              (id +₁ [ g , id ]) ∘ [ f , (id +₁ i₂) ∘ out ]                      ∎

        p-corec : (Y ⇒ X + (D₀ X + Y)) → (Y ⇒ D₀ X)
        p-corec f = p-corec' ([ i₁ , [ i₂ ∘ i₂ , i₂ ∘ i₁ ] ] ∘ f)

        p-corec-commutes : ∀ (f : Y ⇒ X + (D₀ X + Y)) → out ∘ p-corec f ≈ (id +₁ [ id , p-corec f ]) ∘ f
        p-corec-commutes f = begin 
          out ∘ p-corec' ([ i₁ , [ i₂ ∘ i₂ , i₂ ∘ i₁ ] ] ∘ f)                          ≈⟨ p-corec-commutes' ([ i₁ , [ i₂ ∘ i₂ , i₂ ∘ i₁ ] ] ∘ f) ⟩ 
          (id +₁ [ p-corec f , id ]) ∘ [ i₁ , [ i₂ ∘ i₂ , i₂ ∘ i₁ ] ] ∘ f              ≈⟨ pullˡ (∘[] ○ []-cong₂ (inject₁ ○ identityʳ) (∘[] ○ []-cong₂ (extendʳ inject₂) (extendʳ inject₂))) ⟩ 
          [ i₁ , [ i₂ ∘ [ p-corec f , id ] ∘ i₂ , i₂ ∘ [ p-corec f , id ] ∘ i₁ ] ] ∘ f ≈⟨ ([]-cong₂ refl ([]-cong₂ (elimʳ inject₂) (∘-resp-≈ʳ inject₁))) ⟩∘⟨refl ⟩ 
          [ i₁ , [ i₂ , i₂ ∘ p-corec f ] ] ∘ f                                         ≈˘⟨ ([]-cong₂ identityʳ (∘[] ○ []-cong₂ identityʳ refl)) ⟩∘⟨refl ⟩ 
          (id +₁ [ id , p-corec f ]) ∘ f                                               ∎

        p-corec-unique : ∀ (f : Y ⇒ X + (D₀ X + Y)) (g : Y ⇒ D₀ X) → out ∘ g ≈ (id +₁ [ id , g ]) ∘ f → p-corec f ≈ g
        p-corec-unique f g eq = p-corec-unique' ([ i₁ , [ i₂ ∘ i₂ , i₂ ∘ i₁ ] ] ∘ f) g helper
          where
          helper : out ∘ g ≈ (id +₁ [ g , id ]) ∘ [ i₁ , [ i₂ ∘ i₂ , i₂ ∘ i₁ ] ] ∘ f
          helper = begin 
            out ∘ g                                                      ≈⟨ eq ⟩ 
            (id +₁ [ id , g ]) ∘ f                                       ≈˘⟨ ([]-unique (inject₁ ○ identityʳ) (inject₂ ○ ∘[] ○ []-cong₂ identityʳ refl)) ⟩∘⟨refl ⟩ 
            [ i₁ , [ i₂ , i₂ ∘ g ] ] ∘ f                                 ≈˘⟨ ([]-cong₂ refl ([]-cong₂ (elimʳ inject₂) (∘-resp-≈ʳ inject₁))) ⟩∘⟨refl ⟩ 
            [ i₁ , [ i₂ ∘ [ g , id ] ∘ i₂ , i₂ ∘ [ g , id ] ∘ i₁ ] ] ∘ f ≈˘⟨ pullˡ (∘[] ○ []-cong₂ (inject₁ ○ identityʳ) (∘[] ○ []-cong₂ (extendʳ inject₂) (extendʳ inject₂))) ⟩ 
            (id +₁ [ g , id ]) ∘ [ i₁ , [ i₂ ∘ i₂ , i₂ ∘ i₁ ] ] ∘ f      ∎
    open P-Corec

    -- parametrized coiteration as in https://www8.cs.fau.de/ext/milius/publications/files/gmr16_mfps.pdf
    module P-Coit {X Y Z : Obj} where
      abstract
        p-coit : (Y ⇒ Z + Y) → (Z ⇒ X + D₀ X) → (Y ⇒ D₀ X)
        p-coit e f = p-corec ([ [ i₁ , (i₂ ∘ i₁) ] ∘ f , i₂ ∘ i₂ ] ∘ e)

        p-coit-commutes : ∀ (e : Y ⇒ Z + Y) (f : Z ⇒ X + D₀ X) → out ∘ p-coit e f ≈ [ id , i₂ ] ∘ (f +₁ p-coit e f) ∘ e
        p-coit-commutes e f = begin 
          out ∘ p-coit e f                                                                                                                   ≈⟨ p-corec-commutes ([ [ i₁ , (i₂ ∘ i₁) ] ∘ f , i₂ ∘ i₂ ] ∘ e) ⟩ 
          (id +₁ [ id , p-coit e f ]) ∘ [ [ i₁ , (i₂ ∘ i₁) ] ∘ f , i₂ ∘ i₂ ] ∘ e                                                             ≈⟨ pullˡ (∘[] ○ []-cong₂ (pullˡ ∘[]) refl) ⟩ 
          [ [ (id +₁ [ id , p-coit e f ]) ∘ i₁ , (id +₁ [ id , p-coit e f ]) ∘ (i₂ ∘ i₁) ] ∘ f , (id +₁ [ id , p-coit e f ]) ∘ i₂ ∘ i₂ ] ∘ e ≈⟨ ([]-cong₂ 
                                                                                                                                                  (∘-resp-≈ˡ ([]-cong₂ 
                                                                                                                                                                (inject₁ ○ identityʳ) 
                                                                                                                                                                (extendʳ inject₂))) 
                                                                                                                                                  (extendʳ inject₂)) ⟩∘⟨refl ⟩ 
          [ [ i₁ , i₂ ∘ [ id , p-coit e f ] ∘ i₁ ] ∘ f , i₂ ∘ [ id , p-coit e f ] ∘ i₂ ] ∘ e                                                 ≈⟨ ([]-cong₂ (∘-resp-≈ˡ ([]-cong₂ refl (elimʳ inject₁))) (∘-resp-≈ʳ inject₂)) ⟩∘⟨refl ⟩ 
          [ [ i₁ , i₂ ] ∘ f , i₂ ∘ p-coit e f ] ∘ e                                                                                          ≈˘⟨ pullˡ ([]∘+₁ ○ []-cong₂ (∘-resp-≈ˡ (sym +-η)) refl) ⟩ 
          [ id , i₂ ] ∘ (f +₁ p-coit e f) ∘ e                                                                                                ∎
        
        p-coit-unique : ∀ (e : Y ⇒ Z + Y) (f : Z ⇒ X + D₀ X) (g : Y ⇒ D₀ X) → out ∘ g ≈ [ id , i₂ ] ∘ (f +₁ g) ∘ e → p-coit e f ≈ g
        p-coit-unique e f g eq = p-corec-unique ([ [ i₁ , (i₂ ∘ i₁) ] ∘ f , i₂ ∘ i₂ ] ∘ e) g helper
          where
          helper : out ∘ g ≈ (id +₁ [ id , g ]) ∘ [ [ i₁ , (i₂ ∘ i₁) ] ∘ f , i₂ ∘ i₂ ] ∘ e
          helper = begin 
            out ∘ g                                                          ≈⟨ eq ⟩ 
            [ id , i₂ ] ∘ (f +₁ g) ∘ e                                       ≈⟨ pullˡ []∘+₁ ⟩ 
            [ id ∘ f , i₂ ∘ g ] ∘ e                                          ≈˘⟨ ([]-cong₂ (∘-resp-≈ˡ +-η) refl) ⟩∘⟨refl ⟩ 
            [ [ i₁ , i₂ ] ∘ f , i₂ ∘ g ] ∘ e                                 ≈˘⟨ ([]-cong₂ (∘-resp-≈ˡ ([]-cong₂ refl (elimʳ inject₁))) (∘-resp-≈ʳ inject₂)) ⟩∘⟨refl ⟩ 
            [ [ i₁ , i₂ ∘ [ id , g ] ∘ i₁ ] ∘ f , i₂ ∘ [ id , g ] ∘ i₂ ] ∘ e ≈˘⟨ pullˡ (∘[] ○ []-cong₂ (pullˡ (∘[] ○ []-cong₂ (inject₁ ○ identityʳ) (extendʳ inject₂))) (extendʳ inject₂)) ⟩ 
            (id +₁ [ id , g ]) ∘ [ [ i₁ , (i₂ ∘ i₁) ] ∘ f , i₂ ∘ i₂ ] ∘ e    ∎

        p-coit-resp-≈ : ∀ {e e' : Y ⇒ Z + Y} {f f' : Z ⇒ X + D₀ X} → e ≈ e' → f ≈ f' → p-coit e f ≈ p-coit e' f'
        p-coit-resp-≈ {e} {e'} {f} {f'} e≈e' f≈f' = p-coit-unique e f (p-coit e' f') (p-coit-commutes e' f' ○ ∘-resp-≈ʳ (∘-resp-≈ (+₁-cong₂ (sym f≈f') refl) (sym e≈e')))
    open P-Coit

    module D-Kleisli where
      abstract
        extend : ∀ {X Y} → X ⇒ D₀ Y → D₀ X ⇒ D₀ Y
        extend f = p-coit ((f +₁ id) ∘ out) out

        extend-commutes : ∀ {X Y} (f : X ⇒ D₀ Y) → out ∘ extend f ≈ [ out ∘ f , i₂ ∘ extend f ] ∘ out
        extend-commutes {X} {Y} f = p-coit-commutes (((f +₁ id) ∘ out)) out ○ pullˡ ([]∘+₁ ○ []-cong₂ identityˡ refl) ○ pullˡ ([]∘+₁ ○ []-cong₂ refl identityʳ)

        extend-unique : ∀ {X Y} (f : X ⇒ D₀ Y) (g : D₀ X ⇒ D₀ Y) → out ∘ g ≈ [ out ∘ f  , i₂ ∘ g ] ∘ out → extend f ≈ g
        extend-unique f g g-commutes = p-coit-unique ((f +₁ id) ∘ out) out g (g-commutes ○ sym ((pullˡ []∘+₁) ○ pullˡ ([]∘+₁ ○ []-cong₂ (∘-resp-≈ˡ identityˡ) identityʳ)))

        extend-≈ : ∀ {X} {Y} {f g : X ⇒ D₀ Y} → f ≈ g → extend f ≈ extend g
        extend-≈ {X} {Y} {f} {g} f≈g = p-coit-resp-≈ (∘-resp-≈ˡ (+₁-cong₂ f≈g refl)) refl

      kleisli : KleisliTriple C 
      kleisli = record
        { F₀ = D₀ 
        ; unit = now
        ; extend = extend
        ; identityʳ = identityʳ'
        ; identityˡ = extend-unique now id (id-comm ○ (sym ([]-unique (identityˡ ○ sym unitlaw) id-comm-sym)) ⟩∘⟨refl)
        ; assoc = assoc'
        ; sym-assoc = sym assoc'
        ; extend-≈ = extend-≈
        }
        where
          open Terminal
          identityʳ' : ∀ {X Y : Obj} {f : X ⇒ D₀ Y} → extend f ∘ now {X} ≈ f
          identityʳ' {X} {Y} {f} = begin 
            extend f ∘ now                                       ≈⟨ insertˡ out⁻¹∘out ⟩∘⟨refl ⟩ 
            (out⁻¹ ∘ out ∘ extend f) ∘ now                       ≈⟨ (refl⟩∘⟨ (extend-commutes 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ˡ out⁻¹∘out ⟩
            f                                                    ∎

          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ˡ (extend-commutes h) ⟩
            ([ out ∘ h , i₂ ∘ extend h ] ∘ out) ∘ extend g                  ≈⟨ pullʳ (extend-commutes 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ˡ (⟺ (extend-commutes 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         ∎)

      module DK = RMonad kleisli

      p-coit-to-coit : ∀ {X Y Z} (e : Y ⇒ Z + Y) (f : Z ⇒ X + D₀ X) → p-coit e f ≈ extend (out⁻¹ ∘ f) ∘ coit e
      p-coit-to-coit e f = p-coit-unique e f (extend (out⁻¹ ∘ f) ∘ coit e) (begin 
        out ∘ extend (out⁻¹ ∘ f) ∘ coit e                                      ≈⟨ extendʳ (extend-commutes (out⁻¹ ∘ f)) ⟩ 
        [ (out ∘ out⁻¹ ∘ f) , (i₂ ∘ extend (out⁻¹ ∘ f)) ] ∘ out ∘ coit e       ≈⟨ refl⟩∘⟨ coit-commutes e ⟩ 
        [ (out ∘ out⁻¹ ∘ f) , (i₂ ∘ extend (out⁻¹ ∘ f)) ] ∘ (id +₁ coit e) ∘ e ≈⟨ pullˡ []∘+₁ ⟩ 
        [ (out ∘ out⁻¹ ∘ f) ∘ id , (i₂ ∘ extend (out⁻¹ ∘ f)) ∘ coit e ] ∘ e    ≈⟨ ([]-cong₂ identityʳ assoc) ⟩∘⟨refl ⟩ 
        [ out ∘ out⁻¹ ∘ f , i₂ ∘ extend (out⁻¹ ∘ f) ∘ coit e ] ∘ e             ≈⟨ ([]-cong₂ (pullˡ out∘out⁻¹) refl) ⟩∘⟨refl ⟩ 
        [ id ∘ f , i₂ ∘ extend (out⁻¹ ∘ f) ∘ coit e ] ∘ e                      ≈˘⟨ pullˡ []∘+₁ ⟩ 
        [ id , i₂ ] ∘ (f +₁ extend (out⁻¹ ∘ f) ∘ coit e) ∘ e                   ∎)

      module Later∘Extend {X Y} (f : X ⇒ D₀ Y) where
        private
          helper : out ∘ [ f , extend (later ∘ f) ] ∘ out ≈ [ out ∘ f , i₂ ∘ [ f , extend (later ∘ f) ] ∘ out ] ∘ out
          helper = pullˡ ∘[] ○ (([]-cong₂ refl (extend-commutes (later ∘ f) ○ ((([]-cong₂ (pullˡ laterlaw) refl) ⟩∘⟨refl) ○ sym (pullˡ ∘[])))) ⟩∘⟨refl)
          extend-fixpoint : extend f ≈ [ f , extend (later ∘ f) ] ∘ out
          extend-fixpoint = extend-unique f ([ f , extend (later ∘ f) ] ∘ out) helper

        later∘extend : later ∘ extend f ≈ extend (later ∘ f)
        later∘extend = sym (begin 
          extend (later ∘ f)                                          ≈⟨ introˡ out⁻¹∘out ⟩ 
          (out⁻¹ ∘ out) ∘ extend (later ∘ f)                          ≈⟨ pullʳ (extend-commutes (later ∘ f)) ⟩
          out⁻¹ ∘ [ out ∘ later ∘ f , i₂ ∘ extend (later ∘ f) ] ∘ out ≈⟨ refl⟩∘⟨ (([]-cong₂ (pullˡ laterlaw) refl) ○ (sym ∘[])) ⟩∘⟨refl ⟩
          out⁻¹ ∘ (i₂ ∘ [ f , extend (later ∘ f) ]) ∘ out             ≈⟨ refl⟩∘⟨ (pullʳ (sym extend-fixpoint)) ⟩
          out⁻¹ ∘ i₂ ∘ extend f                                       ≈⟨ sym-assoc ⟩
          later ∘ extend f                                            ∎)

        later-extend-comm : later ∘ extend f ≈ extend f ∘ later
        later-extend-comm = sym (begin 
          extend f ∘ later                                    ≈⟨ introˡ out⁻¹∘out ⟩ 
          (out⁻¹ ∘ out) ∘ extend f ∘ later                    ≈⟨ pullʳ (pullˡ (extend-commutes f)) ⟩ 
          out⁻¹ ∘ ([ out ∘ f , i₂ ∘ extend f ] ∘ out) ∘ later ≈⟨ (refl⟩∘⟨ pullʳ laterlaw) ⟩ 
          out⁻¹ ∘ [ out ∘ f , i₂ ∘ extend f ] ∘ i₂            ≈⟨ (refl⟩∘⟨ inject₂) ○ sym-assoc ⟩ 
          later ∘ extend f                                    ∎)

        extend∘later : extend f ∘ later ≈ extend (later ∘ f)
        extend∘later = (sym later-extend-comm) ○ later∘extend
    
    open D-Kleisli

    module D-Monad where
      monad : Monad C
      monad = Kleisli⇒Monad C kleisli

      module D = Monad monad
      D₁ = D.F.₁

      D₁-commutes : ∀ {X Y} (f : X ⇒ Y) → out {Y} ∘ D.F.₁ f ≈ (f +₁ D.F.₁ f) ∘ out {X}
      D₁-commutes {X} {Y} f = begin 
        out ∘ extend (now ∘ f)                          ≈⟨ extend-commutes (now ∘ f) ⟩ 
        [ out ∘ now ∘ f , i₂ ∘ extend (now ∘ f) ] ∘ out ≈⟨ ([]-cong₂ (pullˡ unitlaw) refl) ⟩∘⟨refl ⟩
        (f +₁ extend (now ∘ f)) ∘ out                   ∎

      -- naturality of earlier (out is iso; inner square is the [i₁,out]/D₁-commutes cell)
      earlier-natural : ∀ {X Y} (f : X ⇒ Y) → D₁ f ∘ earlier ≈ earlier ∘ D₁ f
      earlier-natural f = begin
        D₁ f ∘ earlier               ≈⟨ cancelˡ out⁻¹∘out ⟨
        out⁻¹ ∘ out ∘ D₁ f ∘ earlier ≈⟨ refl⟩∘⟨ inner ⟩
        out⁻¹ ∘ out ∘ earlier ∘ D₁ f ≈⟨ cancelˡ out⁻¹∘out ⟩
        earlier ∘ D₁ f               ∎
        where
          inner : out ∘ D₁ f ∘ earlier ≈ out ∘ earlier ∘ D₁ f
          inner = begin
            out ∘ D₁ f ∘ earlier             ≈⟨ extendʳ (D₁-commutes f) ⟩
            (f +₁ D₁ f) ∘ out ∘ earlier      ≈⟨ refl⟩∘⟨ out∘earlier ⟩
            (f +₁ D₁ f) ∘ [ i₁ , out ] ∘ out ≈⟨ extendʳ (∘[] ○ []-cong₂ +₁∘i₁ (sym (D₁-commutes f)) ○ sym []∘+₁) ⟩
            [ i₁ , out ] ∘ (f +₁ D₁ f) ∘ out ≈⟨ refl⟩∘⟨ D₁-commutes f ⟨
            [ i₁ , out ] ∘ out ∘ D₁ f        ≈⟨ extendʳ out∘earlier ⟨
            out ∘ earlier ∘ D₁ f             ∎

      D₁-coit : ∀ {Y Z B} (e : Y ⇒ Z + Y) (g : Z ⇒ B) → D.F.₁ g ∘ coit e ≈ coit ((g +₁ id) ∘ e)
      D₁-coit e g = sym (coit-unique ((g +₁ id) ∘ e) (D.F.₁ g ∘ coit e) (begin 
        out ∘ extend (now ∘ g) ∘ coit e                                ≈⟨ extendʳ (extend-commutes (now ∘ g)) ⟩ 
        [ out ∘ now ∘ g , i₂ ∘ extend (now ∘ g) ] ∘ out ∘ coit e       ≈⟨ refl⟩∘⟨ coit-commutes e ⟩ 
        [ out ∘ now ∘ g , i₂ ∘ extend (now ∘ g) ] ∘ (id +₁ coit e) ∘ e ≈⟨ pullˡ ([]∘+₁ ○ []-cong₂ (identityʳ ○ pullˡ unitlaw) assoc) ⟩ 
        (g +₁ extend (now ∘ g) ∘ coit e) ∘ e                           ≈˘⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ identityˡ identityʳ) ⟩ 
        (id +₁ extend (now ∘ g) ∘ coit e) ∘ (g +₁ id) ∘ e              ∎))

      D₁out⁻¹ : ∀ {X Y} (f : X ⇒ Y) → D₁ f ∘ out⁻¹ ≈ out⁻¹ ∘ (f +₁ D₁ f)
      D₁out⁻¹ f = begin
        D₁ f ∘ out⁻¹                          ≈⟨ introˡ out⁻¹∘out ⟩
        (out⁻¹ ∘ out) ∘ D₁ f ∘ out⁻¹          ≈⟨ pullʳ (pullˡ (D₁-commutes f)) ⟩
        out⁻¹ ∘ ((f +₁ D₁ f) ∘ out) ∘ out⁻¹   ≈⟨ refl⟩∘⟨ cancelʳ out∘out⁻¹ ⟩
        out⁻¹ ∘ (f +₁ D₁ f)                   ∎


    -- helper for proofs
    by-coinduction : ∀ {X Y} {f g : X ⇒ D₀ Y} (α : X ⇒ Y + X) → out ∘ f ≈ (id +₁ f) ∘ α → out ∘ g ≈ (id +₁ g) ∘ α → f ≈ g
    by-coinduction {X} {Y} {f} {g} α eqf eqg = begin 
      f      ≈˘⟨ coit-unique α f eqf ⟩ 
      coit α ≈⟨ coit-unique α g eqg ⟩ 
      g      ∎