module Monad.Instance.Delay {o ℓ e} (ambient : Ambient o ℓ e) where
open Ambient ambient
open M C
open MR C
open Equiv
open HomReasoning
open CoLambek
open F-Coalgebra-Morphism renaming (f to u)
open F-Coalgebra
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-≅)
-- Make DX more accessible outside
D₀ : Obj → Obj
D₀ X = DX {X}
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:
Proving the monad laws then requires two key lemmas, first of all
that the following diagram commutes for any f (this is
extendlaw)
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).
The following module introduces kleisli lifting and some facts about it:
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 ∎
Some helper lemmas:
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ˡ
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 ∎
We will use coinduction as a proof principle for proving strength:
by-coinduction : ∀ {X Y} {f g : X ⇒ D₀ Y} (α : X ⇒ Y + X) → out ∘ f ≈ (idC +₁ f) ∘ α → out ∘ g ≈ (idC +₁ g) ∘ α → f ≈ g
by-coinduction {X} {Y} {f} {g} α eqf eqg = begin
f ≈⟨ sym (Terminal.!-unique (coalgebras Y) (record { f = f ; commutes = eqf })) ⟩
u (Terminal.! (coalgebras Y) {A = record { A = X ; α = α }}) ≈⟨ Terminal.!-unique (coalgebras Y) (record { f = g ; commutes = eqg }) ⟩
g ∎
Next we introduce the proof principle used for proving commutative of Delay: proof by solution uniqueness, i.e. solutions for guarded morphisms are equal:
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) {A = record { A = A (Terminal.⊤ (coalgebras (Y + X))) ; α = [ [ i₁ , h ] , i₂ ] ∘ out }} (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 ∎
Lastly show that Delay is a Kleisli triple:
kleisli : KleisliTriple C
kleisli = record
{ F₀ = D₀
; unit = now
; extend = extend'
; identityʳ = identityʳ'
; identityˡ = extend'-unique now idC (id-comm ○ (sym ([]-unique (identityˡ ○ sym unitlaw) id-comm-sym)) ⟩∘⟨refl)
; 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 ∎
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