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

<!--
```agda
{-# OPTIONS --allow-unsolved-metas #-}
open import Level
open import Categories.FreeObjects.Free
open import Categories.Category.Product renaming (Product to CProduct; _⁂_ to _×C_)
open import Categories.Category
open import Categories.Functor.Core
open import Categories.Adjoint
open import Categories.Adjoint.Properties
open import Categories.Monad
open import Categories.Monad.Strong
open import Category.Instance.AmbientCategory using (Ambient)
open import Categories.NaturalTransformation
open import Categories.Object.Terminal
-- open import Data.Product using (_,_; Σ; Σ-syntax)
```
-->

## 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
  open import Algebra.Properties ambient using (FreeUniformIterationAlgebra; uniformForgetfulF; IsStableFreeUniformIterationAlgebra)

  open Equiv
  open HomReasoning

```

### *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 uniformForgetfulF algebras
    
    adjoint : freeF ⊣ uniformForgetfulF
    adjoint = FO⇒LAdj uniformForgetfulF algebras

    K : Monad C
    K = adjoint⇒monad adjoint
```

### *Proposition 19* If the algebras are stable then K is strong

```agda
  record MonadKStrong : Set (suc o ⊔ suc ℓ ⊔ suc e) where
    field
      algebras : ∀ X → FreeUniformIterationAlgebra X
      stable : ∀ X → IsStableFreeUniformIterationAlgebra (algebras X)
    
    K : Monad C
    K = MonadK.K (record { algebras = algebras })

    open Monad K using (F)
    open Functor F using () renaming (F₀ to K₀; F₁ to K₁)

    KStrong : StrongMonad {C = C} monoidal
    KStrong = record 
      { M = K 
      ; strength = record
        { strengthen = ntHelper (record { η = τ ; commute = commute' }) 
        ; identityˡ = λ {X} → begin 
          K₁ π₂ ∘ τ _ ≈⟨ refl ⟩
          Uniform-Iteration-Algebra-Morphism.h ((algebras (Terminal.⊤ terminal × X) FreeObject.*) (FreeObject.η (algebras X) ∘ π₂)) ∘ τ _ ≈⟨ {!   !} ⟩
          {!   !} ≈⟨ {!   !} ⟩
          {!   !} ≈⟨ {!   !} ⟩
          π₂ ∎
        ; η-comm = λ {A} {B} → begin τ _ ∘ (idC ⁂ η (A , B) B) ≈⟨ τ-η (A , B) ⟩ η (A , B) (A × B) ∎
        ; μ-η-comm = λ {A} {B} → {!   !}
        ; strength-assoc = λ {A} {B} {D} → begin 
          K₁ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ∘ τ _ ≈⟨ {!   !} ⟩ 
          τ _ ∘ (idC ⁂ τ _) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ∎
        }
      }
      where
        open import Agda.Builtin.Sigma
        open IsStableFreeUniformIterationAlgebra using (♯-law; ♯-preserving)

        module _ (P : Category.Obj (CProduct C C)) where
          η = λ Z → FreeObject.η (algebras Z)
          [_,_,_]♯ = λ {A} X Y f → IsStableFreeUniformIterationAlgebra.[_,_]♯ {Y = X} (stable X) {X = A} Y f


          X = fst P
          Y = snd P
          τ : X × K₀ Y ⇒ K₀ (X × Y)
          τ = [ Y , FreeObject.FX (algebras (X × Y)) , η (X × Y) ]♯

          τ-η : τ ∘ (idC ⁂ η Y) ≈ η (X × Y)
          τ-η = sym (♯-law (stable Y) (η (X × Y)))

        [_,_]# : ∀ (A : Uniform-Iteration-Algebra ambient) {X} → (X ⇒ ((Uniform-Iteration-Algebra.A A) + X)) → (X ⇒ Uniform-Iteration-Algebra.A A)
        [ A , f ]# = Uniform-Iteration-Algebra._# A f

        τ-comm : ∀ {X Y Z : Obj} (h : Z ⇒ K₀ Y + Z) → τ (X , Y) ∘ (idC ⁂ [ FreeObject.FX (algebras Y) , h ]#) ≈ [ FreeObject.FX (algebras (X × Y)) , (τ (X , Y) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ]#
        τ-comm {X} {Y} {Z} h = ♯-preserving (stable Y) (η (X , Y) (X × Y)) h

        commute' : ∀ {P₁ : Category.Obj (CProduct C C)} {P₂ : Category.Obj (CProduct C C)} (fg : _[_,_] (CProduct C C) P₁ P₂) 
          → τ P₂ ∘ ((fst fg) ⁂ K₁ (snd fg)) ≈ K₁ ((fst fg) ⁂ (snd fg)) ∘ τ P₁
        commute' {(U , V)} {(W , X)} (f , g) = begin 
          τ _ ∘ (f ⁂ Uniform-Iteration-Algebra-Morphism.h ((algebras V FreeObject.*) (FreeObject.η (algebras X) ∘ g))) ≈⟨ {!   !} ⟩ 
          {!   !} ≈⟨ {!   !} ⟩
          {!   !} ≈⟨ {!   !} ⟩
          Uniform-Iteration-Algebra-Morphism.h ((algebras (U × V) FreeObject.*) (FreeObject.η (algebras (W × X)) ∘ (f ⁂ g))) ∘ τ _ ∎
```