bsc-leon-vatthauer/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.Instance.AmbientCategory 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.UniformIterationAlgebras ambient using (Uniform-Iteration-Algebras)
  open import Algebra.UniformIterationAlgebra ambient using (Uniform-Iteration-Algebra)
  open import Algebra.Properties ambient using (FreeUniformIterationAlgebra; uniformForgetfulF; IsStableFreeUniformIterationAlgebra)

  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 → FreeUniformIterationAlgebra X
      stable : ∀ X → IsStableFreeUniformIterationAlgebra (freealgebras X)

    -- helper for accessing ui-algebras
    algebras : ∀ (X : Obj) → Uniform-Iteration-Algebra
    algebras X = FreeObject.FX (freealgebras X)

    freeF : Functor C Uniform-Iteration-Algebras
    freeF = FO⇒Functor uniformForgetfulF freealgebras
    
    adjoint : freeF ⊣ uniformForgetfulF
    adjoint = FO⇒LAdj uniformForgetfulF 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
```