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
```
-->

# 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)

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

## Definition

The monad is defined by existence of free uniform-iteration algebras. 
Since free objects yield and adjunctions, this yields a monad.

```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
```