mirror of
https://git8.cs.fau.de/theses/bsc-leon-vatthauer.git
synced 2024-05-31 07:28:34 +02:00
27 KiB
27 KiB
module Monad.Instance.Delay {o ℓ e} (ambient : Ambient o ℓ e) where
open Ambient ambient
Definition
The delay monad is usually defined as a coinductive type with two constructors now : X → D X and later : D X → D X, e.g. in the agda-stdlib
We will now define it categorically by existence of final coalgebras for the functor (X + -) where X is some object.
This functor trivially sends objects Y to X + Y and functions f to id + f.
In this definition D X is the underlying object of the final coalgebra given by X.
We then use Lambek's Lemma to gain an isomorphism D X ≅ X + D X, whose inverse can be factored into the constructors now and later.
record DelayM : Set (o ⊔ ℓ ⊔ e) where
field
coalgebras : ∀ (A : Obj) → Terminal (F-Coalgebras (A +-))
module _ {X : Obj} where
open Terminal (coalgebras X) using (⊤; !; !-unique)
open F-Coalgebra ⊤ using () renaming (A to DX) public
out-≅ : DX ≅ X + DX
out-≅ = colambek {F = X +- } (coalgebras 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₂
-- convenient notation
▷ = later
unitlaw : out ∘ now ≈ i₁
unitlaw = cancelˡ (_≅_.isoʳ out-≅)
laterlaw : out ∘ later ≈ i₂
laterlaw = cancelˡ (_≅_.isoʳ out-≅)
Since Y ⇒ X + Y is an algebra for the (X + -) functor, we can use the final coalgebras to get a coiteration operator coit:
module _ {Y : Obj} where
coit : Y ⇒ X + Y → Y ⇒ DX
coit f = u (! {A = record { A = Y ; α = f }})
coit-commutes : ∀ (f : Y ⇒ X + Y) → out ∘ (coit f) ≈ (idC +₁ coit f) ∘ f
coit-commutes f = commutes (! {A = record { A = Y ; α = f }})
coit-resp-≈ : ∀ {f g : Y ⇒ X + Y} → f ≈ g → coit f ≈ coit g
coit-resp-≈ {f} {g} eq = Terminal.!-unique (coalgebras X) (record { f = coit g ; commutes = begin
out ∘ coit g ≈⟨ coit-commutes g ⟩
(idC +₁ coit g) ∘ g ≈⟨ (refl⟩∘⟨ sym eq) ⟩
(idC +₁ coit g) ∘ f ∎ })
Furthermore 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 (Y + \_)-functor defined above, this gives us another morphism ι : X × N ⇒ DX by using the final coalgebras.
ι-coalg : F-Coalgebra-Morphism (record { A = X × N ; α = _≅_.from nno-iso }) (record { A = DX ; α = out })
ι-coalg = ! {A = record { A = X × N ; α = _≅_.from nno-iso }}
ι : X × N ⇒ DX
ι = u ι-coalg
ι-commutes : out ∘ ι ≈ (idC +₁ ι) ∘ _≅_.from nno-iso
ι-commutes = commutes ι-coalg
## Delay is a monad
The next step is showing that this actually yields a monad. Some parts for this are already given, we can construct `D X` from `X` and `now : D X ⇒ D X` is the monad unit.
What's missing is Kleisli-lifting, given a morphism `f : X ⇒ D Y` we need to construct a morphism `extend f : D X ⇒ D Y`.
To do so we go from `D X` to `D X + D Y` via injection and then construct a coalgebra `D X + D Y ⇒ Y + (D X + D Y)`, the final coalgebra `D Y ⇒ Y + D Y` then yields a coalgebra-morphism from `D X + D Y` to `D Y`, see the following diagram:
<!-- https://q.uiver.app/#q=WzAsNSxbMCwxLCJEWCArIERZIl0sWzIsMSwiWSArIChEWCArIERZKSJdLFswLDAsIkRYIl0sWzAsMiwiRFkiXSxbMiwyLCJZICsgRFkiXSxbMCwxLCJcXGFscGhhIl0sWzIsMCwiaV8xIl0sWzAsMywiISIsMCx7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImRhc2hlZCJ9fX1dLFszLDQsIm91dCJdLFsxLDQsIkYgISIsMCx7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImRhc2hlZCJ9fX1dXQ== -->
<iframe class="quiver-embed" src="https://q.uiver.app/#q=WzAsNSxbMCwxLCJEWCArIERZIl0sWzIsMSwiWSArIChEWCArIERZKSJdLFswLDAsIkRYIl0sWzAsMiwiRFkiXSxbMiwyLCJZICsgRFkiXSxbMCwxLCJcXGFscGhhIl0sWzIsMCwiaV8xIl0sWzAsMywiISIsMCx7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImRhc2hlZCJ9fX1dLFszLDQsIm91dCJdLFsxLDQsIkYgISIsMCx7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImRhc2hlZCJ9fX1dXQ==&embed" width="551" height="304" style="border-radius: 8px; border: none;"></iframe>
Proving the monad laws then requires two key lemmas, first of all that the following diagram commutes for any `f` (this is `extendlaw`)
<!-- https://q.uiver.app/#q=WzAsNCxbMCwwLCJEWCJdLFszLDAsIkRZIl0sWzAsMSwiWCArIERYIl0sWzMsMSwiWSArIERZIl0sWzAsMSwiZXh0ZW5kXFw7ZiJdLFswLDIsIm91dCIsMl0sWzIsMywiW291dFxcO2YsaV8yXFw7KGV4dGVuZFxcO2YpXSIsMl0sWzEsMywib3V0Il1d -->
<iframe class="quiver-embed" src="https://q.uiver.app/#q=WzAsNCxbMCwwLCJEWCJdLFszLDAsIkRZIl0sWzAsMSwiWCArIERYIl0sWzMsMSwiWSArIERZIl0sWzAsMSwiZXh0ZW5kXFw7ZiJdLFswLDIsIm91dCIsMl0sWzIsMywiW291dFxcO2YsaV8yXFw7KGV4dGVuZFxcO2YpXSIsMl0sWzEsMywib3V0Il1d&embed" width="670" height="304" style="border-radius: 8px; border: none;"></iframe>
and second that `extend f` is the unique morphism satisfying the commutative diagram i.e. any other morphism for which the diagram commutes must be equivalent to `extend f` (this is `extend-unique`).
```agda
-- Make DX more accessible outside
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 ∎
-- Lemma 39: ▷ ∘ f* ≈ (▷ ∘ f)* ≈ f* ∘ ▷
module _ {X Y} (f : X ⇒ D₀ Y) where
private
helper : out ∘ [ f , extend' (▷ ∘ f) ] ∘ out ≈ [ out ∘ f , i₂ ∘ [ f , extend' (▷ ∘ f) ] ∘ out ] ∘ out
helper = pullˡ ∘[] ○ (([]-cong₂ refl (extendlaw (▷ ∘ f) ○ ((([]-cong₂ (pullˡ laterlaw) refl) ⟩∘⟨refl) ○ sym (pullˡ ∘[])))) ⟩∘⟨refl)
helper₁ : [ f , extend' (▷ ∘ f) ] ∘ out ≈ extend' f
helper₁ = sym (extend'-unique f ([ f , extend' (▷ ∘ f) ] ∘ out) helper)
▷∘extendˡ : ▷ ∘ extend' f ≈ extend' (▷ ∘ f)
▷∘extendˡ = sym (begin
extend' (▷ ∘ f) ≈⟨ introˡ (_≅_.isoˡ out-≅) ⟩
(out⁻¹ ∘ out) ∘ extend' (▷ ∘ f) ≈⟨ pullʳ (extendlaw (▷ ∘ f)) ⟩
out⁻¹ ∘ [ out ∘ ▷ ∘ f , i₂ ∘ extend' (▷ ∘ f) ] ∘ out ≈⟨ (refl⟩∘⟨ (([]-cong₂ (pullˡ laterlaw) refl) ○ (sym ∘[])) ⟩∘⟨refl) ⟩
out⁻¹ ∘ (i₂ ∘ [ f , extend' (▷ ∘ f) ]) ∘ out ≈⟨ (refl⟩∘⟨ (pullʳ helper₁)) ⟩
out⁻¹ ∘ i₂ ∘ extend' f ≈⟨ sym-assoc ⟩
▷ ∘ extend' f ∎)
▷∘extend-comm : ▷ ∘ extend' f ≈ extend' f ∘ ▷
▷∘extend-comm = sym (begin
extend' f ∘ ▷ ≈⟨ introˡ (_≅_.isoˡ out-≅) ⟩
(out⁻¹ ∘ out) ∘ extend' f ∘ ▷ ≈⟨ pullʳ (pullˡ (extendlaw f)) ⟩
out⁻¹ ∘ ([ out ∘ f , i₂ ∘ extend' f ] ∘ out) ∘ ▷ ≈⟨ (refl⟩∘⟨ pullʳ laterlaw) ⟩
out⁻¹ ∘ [ out ∘ f , i₂ ∘ extend' f ] ∘ i₂ ≈⟨ (refl⟩∘⟨ inject₂) ○ sym-assoc ⟩
▷ ∘ extend' f ∎)
▷∘extendʳ : extend' f ∘ ▷ ≈ extend' (▷ ∘ f)
▷∘extendʳ = (sym ▷∘extend-comm) ○ ▷∘extendˡ
is-guarded : ∀ {X Y} (g : X ⇒ D₀ (Y + X)) → Set (ℓ ⊔ e)
is-guarded {X} {Y} g = ∃[ h ] (i₁ +₁ idC) ∘ h ≈ out ∘ g
guarded-unique : ∀ {X Y} (g : X ⇒ D₀ (Y + X)) (f i : X ⇒ D₀ Y) → is-guarded g → f ≈ extend' ([ now , f ]) ∘ g → i ≈ extend' ([ now , i ]) ∘ g → f ≈ i
guarded-unique {X} {Y} g f i (h , guarded) eqf eqi = begin
f ≈⟨ eqf ⟩
extend' ([ now , f ]) ∘ g ≈⟨ (sym (Terminal.!-unique (coalgebras Y) (record { f = extend' ([ now , f ]) ; commutes = begin
out ∘ extend' ([ now , f ]) ≈⟨ extendlaw ([ now , f ]) ⟩
[ out ∘ [ now , f ] , i₂ ∘ extend' ([ now , f ]) ] ∘ out ≈⟨ ([]-cong₂ ∘[] refl) ⟩∘⟨refl ⟩
[ [ out ∘ now , out ∘ f ] , i₂ ∘ extend' ([ now , f ]) ] ∘ out ≈⟨ ([]-cong₂ ([]-cong₂ unitlaw (helper f eqf)) refl) ⟩∘⟨refl ⟩
[ [ i₁ , (idC +₁ extend' ([ now , f ])) ∘ h ] , i₂ ∘ extend' ([ now , f ]) ] ∘ out ≈˘⟨ ([]-cong₂ ([]-cong₂ identityʳ refl) refl) ⟩∘⟨refl ⟩
[ [ i₁ ∘ idC , (idC +₁ extend' ([ now , f ])) ∘ h ] , i₂ ∘ extend' ([ now , f ]) ] ∘ out ≈˘⟨ ([]-cong₂ ([]-cong₂ +₁∘i₁ refl) refl) ⟩∘⟨refl ⟩
[ [ (idC +₁ extend' ([ now , f ])) ∘ i₁ , (idC +₁ extend' ([ now , f ])) ∘ h ] , i₂ ∘ extend' ([ now , f ]) ] ∘ out ≈˘⟨ ([]-cong₂ ∘[] +₁∘i₂) ⟩∘⟨refl ⟩
[ (idC +₁ extend' ([ now , f ])) ∘ [ i₁ , h ] , (idC +₁ extend' ([ now , f ])) ∘ i₂ ] ∘ out ≈˘⟨ pullˡ ∘[] ⟩
(idC +₁ extend' ([ now , f ])) ∘ [ [ i₁ , h ] , i₂ ] ∘ out ∎ }))) ⟩∘⟨refl ⟩
u (Terminal.! (coalgebras Y)) ∘ g ≈⟨ (Terminal.!-unique (coalgebras Y) (record { f = extend' ([ now , i ]) ; commutes = begin
out ∘ extend' ([ now , i ]) ≈⟨ extendlaw ([ now , i ]) ⟩
[ out ∘ [ now , i ] , i₂ ∘ extend' ([ now , i ]) ] ∘ out ≈⟨ ([]-cong₂ ∘[] refl) ⟩∘⟨refl ⟩
[ [ out ∘ now , out ∘ i ] , i₂ ∘ extend' ([ now , i ]) ] ∘ out ≈⟨ ([]-cong₂ ([]-cong₂ unitlaw (helper i eqi)) refl) ⟩∘⟨refl ⟩
[ [ i₁ , (idC +₁ extend' ([ now , i ])) ∘ h ] , i₂ ∘ extend' ([ now , i ]) ] ∘ out ≈˘⟨ ([]-cong₂ ([]-cong₂ identityʳ refl) refl) ⟩∘⟨refl ⟩
[ [ i₁ ∘ idC , (idC +₁ extend' ([ now , i ])) ∘ h ] , i₂ ∘ extend' ([ now , i ]) ] ∘ out ≈˘⟨ ([]-cong₂ ([]-cong₂ +₁∘i₁ refl) refl) ⟩∘⟨refl ⟩
[ [ (idC +₁ extend' ([ now , i ])) ∘ i₁ , (idC +₁ extend' ([ now , i ])) ∘ h ] , i₂ ∘ extend' ([ now , i ]) ] ∘ out ≈˘⟨ ([]-cong₂ ∘[] +₁∘i₂) ⟩∘⟨refl ⟩
[ (idC +₁ extend' ([ now , i ])) ∘ [ i₁ , h ] , (idC +₁ extend' ([ now , i ])) ∘ i₂ ] ∘ out ≈˘⟨ pullˡ ∘[] ⟩
(idC +₁ extend' ([ now , i ])) ∘ [ [ i₁ , h ] , i₂ ] ∘ out ∎ })) ⟩∘⟨refl ⟩
extend' ([ now , i ]) ∘ g ≈⟨ sym eqi ⟩
i ∎
where
helper : ∀ (f : X ⇒ D₀ Y) → f ≈ extend' ([ now , f ]) ∘ g → out ∘ f ≈ (idC +₁ extend' ([ now , f ])) ∘ h
helper f eqf = begin
out ∘ f ≈⟨ refl⟩∘⟨ eqf ⟩
out ∘ extend' ([ now , f ]) ∘ g ≈⟨ pullˡ (extendlaw ([ now , f ])) ⟩
([ out ∘ [ now , f ] , i₂ ∘ extend' ([ now , f ]) ] ∘ out) ∘ g ≈⟨ pullʳ (sym guarded) ⟩
[ out ∘ [ now , f ] , i₂ ∘ extend' ([ now , f ]) ] ∘ (i₁ +₁ idC) ∘ h ≈⟨ pullˡ []∘+₁ ⟩
[ (out ∘ [ now , f ]) ∘ i₁ , (i₂ ∘ extend' ([ now , f ])) ∘ idC ] ∘ h ≈⟨ ([]-cong₂ (pullʳ inject₁) identityʳ) ⟩∘⟨refl ⟩
[ out ∘ now , i₂ ∘ extend' ([ now , f ]) ] ∘ h ≈⟨ ([]-cong₂ (unitlaw ○ sym identityʳ) refl) ⟩∘⟨refl ⟩
(idC +₁ extend' ([ now , f ])) ∘ h ∎
out-law : ∀ {X Y} (f : X ⇒ Y) → out {Y} ∘ extend' (now ∘ f) ≈ (f +₁ extend' (now ∘ f)) ∘ out {X}
out-law {X} {Y} f = begin
out ∘ extend' (now ∘ f) ≈⟨ extendlaw (now ∘ f) ⟩
[ out ∘ now ∘ f , i₂ ∘ extend' (now ∘ f) ] ∘ out ≈⟨ ([]-cong₂ (pullˡ unitlaw) refl) ⟩∘⟨refl ⟩
(f +₁ extend' (now ∘ f)) ∘ out ∎
kleisli : KleisliTriple C
kleisli = record
{ F₀ = D₀
; unit = now
; extend = extend'
; identityʳ = identityʳ'
; identityˡ = identityˡ'
; assoc = assoc'
; sym-assoc = sym assoc'
; extend-≈ = extend-≈'
}
where
open Terminal
α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 (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ʳ ⟩
α (alg g) ≈⟨ ⟺ (αf≈αg eq) ⟩
α (alg f) ≈˘⟨ elimˡ identity ⟩
(idC +₁ idC) ∘ α (alg f) ∎ }
; to = record { f = idC ; commutes = begin
α (alg f) ∘ idC ≈⟨ identityʳ ⟩
α (alg f) ≈⟨ αf≈αg eq ⟩
α (alg g) ≈˘⟨ elimˡ identity ⟩
(idC +₁ idC) ∘ α (alg g) ∎ }
; iso = record
{ isoˡ = identity²
; isoʳ = identity²
}
}
where open Functor (Y +-) using (identity)
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₁ ⟩
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}))) ⟩
((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 ⟩
(idC +₁ (u (! (coalgebras X) {A = alg now}))) ∘ [ i₁ , i₂ ∘ i₁ ] ∘ out ≈⟨ pullˡ ∘[] ⟩
[ (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 ∎ })
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} 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ʳ ⟩
α (⊤ (coalgebras Y)) ∘ u (! (coalgebras Y)) ≈⟨ commutes (! (coalgebras Y)) ⟩
(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 ⟩
extend' g ∎
monad : Monad C
monad = Kleisli⇒Monad C kleisli
-- redundant but convenient to have
functor : Endofunctor C
functor = Monad.F monad