bsc-leon-vatthauer/agda/src/Monad/Instance/K.lagda.md

<!--
```agda
open import Level
open import Categories.FreeObjects.Free using (FreeObject; FO⇒Functor; FO⇒LAdj)
open import Categories.Functor.Core using (Functor)
open import Categories.Adjoint using (_⊣_)
open import Categories.Adjoint.Properties using (adjoint⇒monad)
open import Categories.Monad using (Monad)
open import Categories.Monad.Relative using () renaming (Monad to RMonad)
open import Category.Ambient using (Ambient)
open import Categories.Monad.Construction.Kleisli
open import Categories.Category.Cartesian using (Cartesian)
open import Categories.Category.BinaryProducts using (BinaryProducts)
```
-->

# The monad K

```agda
module Monad.Instance.K {o ℓ e} (ambient : Ambient o ℓ e) where
  open Ambient ambient
  open import Category.Construction.ElgotAlgebras cocartesian
  open import Algebra.Elgot cocartesian using (Elgot-Algebra)
  open import Algebra.Elgot.Free cocartesian using (FreeElgotAlgebra; elgotForgetfulF)
  open import Algebra.Elgot.Stable distributive using (IsStableFreeElgotAlgebra; IsStableFreeElgotAlgebraˡ; isStable⇒isStableˡ)

  -- open Cartesian cartesian
  -- open BinaryProducts products

  open Equiv
  open MR C
  open M C
  open HomReasoning
```

## Definition
Existence of stable free Elgot algebras yields the monad K

```agda
  record MonadK : Set (suc o ⊔ suc ℓ ⊔ suc e) where
    field
      freealgebras : ∀ X → FreeElgotAlgebra X
      stable : ∀ X → IsStableFreeElgotAlgebra (freealgebras X)

    -- helper for accessing elgot algebras
    algebras : ∀ (X : Obj) → Elgot-Algebra
    algebras X = FreeObject.FX (freealgebras X)

    freeF : Functor C Elgot-Algebras
    freeF = FO⇒Functor elgotForgetfulF freealgebras
    
    adjoint : freeF ⊣ elgotForgetfulF
    adjoint = FO⇒LAdj elgotForgetfulF freealgebras

    monadK : Monad C
    monadK = adjoint⇒monad adjoint
    module monadK = Monad monadK

    kleisliK : KleisliTriple C
    kleisliK = Monad⇒Kleisli C monadK
    module kleisliK = RMonad kleisliK

    module K = Functor monadK.F
```

Uniqueness of the stability operator gives us the following proof principle:

```agda
    open Elgot-Algebra using () renaming (A to ⟦_⟧)
    private
      -- some helper definitions to make our life easier
      η = λ Z → FreeObject.η (freealgebras Z)
      stableˡ = λ X → isStable⇒isStableˡ (freealgebras X) (stable X)
      _# = λ {A} {X} f → Elgot-Algebra._# (algebras A) {X = X} f

    by-stability : ∀ {X Y A} {f g : X × ⟦ algebras Y ⟧ ⇒ ⟦ algebras A ⟧} (i : X × Y ⇒ ⟦ algebras A ⟧) 
                    → i ≈ f ∘ (idC ⁂ η Y) 
                    → i ≈ g ∘ (idC ⁂ η Y) 
                    → (∀ {Z} (h : Z ⇒ ⟦ algebras Y ⟧ + Z) → f ∘ (idC ⁂ (Elgot-Algebra._# (algebras Y) h)) ≈ Elgot-Algebra._# (algebras A) ((f +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)))
                    → (∀ {Z} (h : Z ⇒ ⟦ algebras Y ⟧ + Z) → g ∘ (idC ⁂ (Elgot-Algebra._# (algebras Y) h)) ≈ Elgot-Algebra._# (algebras A) ((g +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)))
                    → f ≈ g
    by-stability {X} {Y} {A} {f} {g} i f-law g-law f-pres g-pres = begin 
      f ≈⟨ ♯-unique i f f-law f-pres ⟩ 
      [ algebras A , i ]♯ ≈⟨ sym (♯-unique i g g-law g-pres) ⟩ 
      g ∎
      where
      open IsStableFreeElgotAlgebra (stable Y) using ([_,_]♯; ♯-unique)

    by-stabilityˡ : ∀ {X Y} {A : Elgot-Algebra} {f g : ⟦ algebras Y ⟧ × X ⇒ ⟦ A ⟧} (i : Y × X ⇒ ⟦ A ⟧) 
                    → i ≈ f ∘ (η Y ⁂ idC) 
                    → i ≈ g ∘ (η Y ⁂ idC) 
                    → (∀ {Z} (h : Z ⇒ ⟦ algebras Y ⟧ + Z) → f ∘ (h # ⁂ idC) ≈ Elgot-Algebra._# A ((f +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC)))
                    → (∀ {Z} (h : Z ⇒ ⟦ algebras Y ⟧ + Z) → g ∘ (h # ⁂ idC) ≈ Elgot-Algebra._# A ((g +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC)))
                    → f ≈ g
    by-stabilityˡ {X} {Y} {A} {f} {g} i f-law g-law f-pres g-pres = begin 
      f ≈⟨ ♯ˡ-unique i f f-law f-pres ⟩ 
      [ A , i ]♯ˡ ≈⟨ sym (♯ˡ-unique i g g-law g-pres) ⟩ 
      g ∎
      where
      open IsStableFreeElgotAlgebraˡ (stableˡ Y) using ([_,_]♯ˡ; ♯ˡ-unique)
```