The Monad K

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

Existence of stable free Elgot algebras yields the monad K

  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

Some helper definitions to make our life easier

    open Elgot-Algebra using (#-resp-≈; #-Fixpoint; #-Compositionality; #-Uniformity; #-Folding; #-Diamond; #-Stutter) renaming (A to ⟦_⟧) public
    stableˡ = λ X → isStable⇒isStableˡ (freealgebras X) (stable X)
    η = λ Z → FreeObject.η (freealgebras Z)
    _♯ = λ {A X Y} f → IsStableFreeElgotAlgebra.[_,_]♯ {Y = X} (stable X) {X = A} (algebras Y) f
    _♯ˡ = λ {A X Y} f → IsStableFreeElgotAlgebraˡ.[_,_]♯ˡ {Y = X} (stableˡ X) {X = A} (algebras Y) f
    _# = λ {A} {X} f → Elgot-Algebra._# (algebras A) {X = X} f

The kleisli star is iteration preserving:

    open kleisliK using (extend)
    open monadK using (μ)
    
    extend-preserve : ∀ {X Y Z} (f : X ⇒ K.₀ Y) (h : Z ⇒ K.₀ X + Z) → extend f ∘ h # ≈ ((extend f +₁ idC) ∘ h) #
    extend-preserve {X} {Y} {Z} f h = begin
      (μ.η _ ∘ K.₁ f) ∘ h #                   ≈⟨ pullʳ (Elgot-Algebra-Morphism.preserves (((freealgebras _) FreeObject.*) (η _ ∘ f))) ⟩
      μ.η _ ∘ ((K.₁ f +₁ idC) ∘ h) #          ≈⟨ Elgot-Algebra-Morphism.preserves (((freealgebras _) FreeObject.*) idC) ⟩
      ((μ.η _ +₁ idC) ∘ (K.₁ f +₁ idC) ∘ h) # ≈⟨ #-resp-≈ (algebras _) (pullˡ (+₁∘+₁ ○ +₁-cong₂ refl identity²)) ⟩
      ((extend f +₁ idC) ∘ h) #               ∎

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

    by-stability : ∀ {X Y} (A : Elgot-Algebra) {f g : X × ⟦ algebras Y ⟧ ⇒ ⟦ A ⟧} (i : X × Y ⇒ ⟦ A ⟧)
                    → i ≈ f ∘ (idC ⁂ η Y) 
                    → i ≈ g ∘ (idC ⁂ η Y) 
                    → (∀ {Z} (h : Z ⇒ ⟦ algebras Y ⟧ + Z) → f ∘ (idC ⁂ (Elgot-Algebra._# (algebras Y) h)) ≈ Elgot-Algebra._# A ((f +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)))
                    → (∀ {Z} (h : Z ⇒ ⟦ algebras Y ⟧ + Z) → g ∘ (idC ⁂ (Elgot-Algebra._# (algebras Y) h)) ≈ Elgot-Algebra._# 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 ⟩ 
      [ 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 ∘ ((Elgot-Algebra._# (algebras Y) h) ⁂ idC) ≈ Elgot-Algebra._# A ((f +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC)))
                    → (∀ {Z} (h : Z ⇒ ⟦ algebras Y ⟧ + Z) → g ∘ ((Elgot-Algebra._# (algebras Y) 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)