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

<!--
```agda
open import Level
open import Categories.Category.Equivalence using (StrongEquivalence)
open import Function using (id)
open import Categories.FreeObjects.Free
open import Categories.Functor.Core
open import Categories.Adjoint
open import Categories.Adjoint.Properties
open import Categories.Adjoint.Monadic.Crude
open import Categories.NaturalTransformation.Core renaming (id to idN)
open import Categories.Monad
open import Categories.Category.Construction.EilenbergMoore
open import Categories.Category.Slice
open import Category.Instance.AmbientCategory using (Ambient)
```
-->

## Summary
In this file I explore the monad ***K*** and its properties:

- [X] *Lemma 16* Definition of the monad
- [ ] *Lemma 16* EilenbergMoore⇒UniformIterationAlgebras (use [crude monadicity theorem](https://agda.github.io/agda-categories/Categories.Adjoint.Monadic.Crude.html))
- [ ] *Proposition 19* ***K*** is strong
- [ ] *Theorem 22* ***K*** is an equational lifting monad
- [ ] *Proposition 23* The Kleisli category of ***K*** is enriched over pointed partial orders and strict monotone maps
- [ ] *Proposition 25* ***K*** is copyable and weakly discardable
- [ ] *Theorem 29* ***K*** is an initial pre-Elgot monad and an initial strong pre-Elgot monad


## Code

```agda
module Monad.Instance.K {o ℓ e} (ambient : Ambient o ℓ e) where
  open Ambient ambient
  open import Category.Construction.UniformIterationAlgebras ambient
  open import Algebra.UniformIterationAlgebra ambient
  open Equiv

  -- TODO move this to a different file

  forgetfulF : Functor Uniform-Iteration-Algebras C
  forgetfulF = record
    { F₀ = λ X → Uniform-Iteration-Algebra.A X
    ; F₁ = λ f → Uniform-Iteration-Algebra-Morphism.h f
    ; identity = refl
    ; homomorphism = refl
    ; F-resp-≈ = id
    }

  -- typedef
  FreeUniformIterationAlgebra : Obj → Set (suc o ⊔ suc ℓ ⊔ suc e)
  FreeUniformIterationAlgebra X = FreeObject {C = C} {D = Uniform-Iteration-Algebras} forgetfulF X

```

### *Lemma 16*: definition of monad ***K***

```agda
  record MonadK : Set (suc o ⊔ suc ℓ ⊔ suc e) where
    field
      algebras : ∀ X → FreeUniformIterationAlgebra X

    freeF : Functor C Uniform-Iteration-Algebras
    freeF = FO⇒Functor forgetfulF algebras
    
    adjoint : freeF ⊣ forgetfulF
    adjoint = FO⇒LAdj forgetfulF algebras

    K : Monad C
    K = adjoint⇒monad adjoint

    -- EilenbergMoore⇒UniformIterationAlgebras : StrongEquivalence (EilenbergMoore K) (Uniform-Iteration-Algebras D)
    -- EilenbergMoore⇒UniformIterationAlgebras = {!   !}
```