open import Level
open import Categories.FreeObjects.Free
open import Categories.Category.Product using () renaming (Product to CProduct; _⁂_ to _×C_)
open import Data.Product using (_,_; proj₁; proj₂)
open import Categories.Category
open import Categories.Functor.Core
open import Categories.Adjoint
open import Categories.Adjoint.Properties
open import Categories.Monad hiding (id)
open import Categories.Monad.Strong
open import Categories.Monad.Relative renaming (Monad to RMonad)
open import Categories.Category.Distributive
open import Categories.NaturalTransformation hiding (id)
open import Categories.Object.Terminal
open import Monad.Helper

import Monad.Instance.K as MIK
import Categories.Morphism as M
import Categories.Morphism.Reasoning as MR


-- K is a Strong Monad

module Monad.Instance.K.Strong {o ℓ e} {C : Category o ℓ e} (distributive : Distributive C) (MK : MIK.MonadK distributive) where
  open import Category.Distributive.Helper distributive
  open Bundles
  open import Category.Construction.ElgotAlgebras cocartesian
  open import Algebra.Elgot cocartesian
  open import Algebra.Elgot.Free cocartesian using (FreeElgotAlgebra; elgotForgetfulF)
  open import Algebra.Elgot.Stable distributive using (IsStableFreeElgotAlgebra)

  open MIK distributive
  open Category C
  open MonadK MK
  open Equiv
  open MR C
  open M C
  open HomReasoning

  -- we use properties of the kleisli representation as well as the 'normal' monad representation
  open kleisliK using (extend)
  open monadK using (μ)

  open IsStableFreeElgotAlgebra using (♯-law; ♯-preserving; ♯-unique)

  module _ (P : Category.Obj (CProduct C C)) where
    private
      X = proj₁ P
      Y = proj₂ P
    τ : X × K.₀ Y ⇒ K.₀ (X × Y)
    τ = η (X × Y) ♯

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

    -- for K not only strengthening with 1 is irrelevant
    τ-π₂ : K.₁ π₂ ∘ τ ≈ π₂
    τ-π₂ = begin 
      K.₁ π₂ ∘ τ ≈⟨ ♯-unique (stable Y) (η _ ∘ π₂) (K.₁ π₂ ∘ τ) comm₁ comm₂ ⟩
      (η _ ∘ π₂) ♯ ≈⟨ sym (♯-unique (stable Y) (η _ ∘ π₂) π₂ (sym π₂∘⁂) comm₃) ⟩
      π₂ ∎
      where
      comm₁ : η _ ∘ π₂ ≈ (K.₁ π₂ ∘ τ) ∘ (id ⁂ η _)
      comm₁ = sym (begin 
        (K.₁ π₂ ∘ τ) ∘ (id ⁂ η _) ≈⟨ pullʳ τ-η ⟩ 
        K.₁ π₂ ∘ η _                 ≈⟨ (sym (F₁⇒extend monadK π₂)) ⟩∘⟨refl ⟩
        extend (η _ ∘ π₂) ∘ η _                              ≈⟨ kleisliK.identityʳ ⟩
        η _ ∘ π₂                                             ∎)
      comm₂ : ∀ {Z : Obj} (h : Z ⇒ K.₀ Y + Z) → (K.₁ π₂ ∘ τ) ∘ (id ⁂ h # ) ≈ ((K.₁ π₂ ∘ τ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ h))#
      comm₂ {Z} h = begin
        (K.₁ π₂ ∘ τ) ∘ (id ⁂ h #)                                   ≈⟨ pullʳ (♯-preserving (stable Y) (η _) h) ⟩ 
        K.₁ π₂ ∘ ((τ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ h)) #          ≈⟨ Elgot-Algebra-Morphism.preserves ((freealgebras (X × Y) FreeObject.*) (η _ ∘ π₂)) ⟩
        ((K.₁ π₂ +₁ id) ∘ (τ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ h)) # ≈⟨ #-resp-≈ (algebras Y) (pullˡ (+₁∘+₁ ○ +₁-cong₂ refl identity²)) ⟩
        ((K.₁ π₂ ∘ τ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ h))#           ∎
      comm₃ : ∀ {Z : Obj} (h : Z ⇒ K.₀ Y + Z) → π₂ ∘ (id ⁂ h #) ≈ ((π₂ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ h)) #
      comm₃ {Z} h = begin 
        π₂ ∘ (id ⁂ h #)                            ≈⟨ π₂∘⁂ ⟩ 
        h # ∘ π₂                                    ≈⟨ sym (#-Uniformity (algebras Y) uni-helper) ⟩ 
        ((π₂ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ h)) # ∎
        where
        uni-helper = begin 
          (id +₁ π₂) ∘ (π₂ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ h) ≈⟨ pullˡ +₁∘+₁ ⟩ 
          (id ∘ π₂ +₁ π₂ ∘ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ h)    ≈⟨ (+₁-cong₂ identityˡ identityʳ) ⟩∘⟨refl ⟩ 
          (π₂ +₁ π₂) ∘ distributeˡ⁻¹ ∘ (id ⁂ h)                ≈⟨ pullˡ distributeˡ⁻¹-π₂ ⟩ 
          π₂ ∘ (id ⁂ h)                                        ≈⟨ project₂ ⟩ 
          h ∘ π₂                                                ∎

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

  K₁η : ∀ {X Y} (f : X ⇒ Y) → K.₁ f ∘ η X ≈ η Y ∘ f
  K₁η {X} {Y} f = begin 
    K.₁ f ∘ η X            ≈⟨ (sym (F₁⇒extend monadK f)) ⟩∘⟨refl ⟩ 
    extend (η Y ∘ f) ∘ η X ≈⟨ kleisliK.identityʳ ⟩ 
    η Y ∘ f                ∎

  KStrength : Strength monoidal monadK

  Strength.strengthen KStrength = ntHelper (record { η = τ ; commute = commute' })
    where
    commute' : ∀ {P₁ : Category.Obj (CProduct C C)} {P₂ : Category.Obj (CProduct C C)} (fg : _[_,_] (CProduct C C) P₁ P₂) 
      → τ P₂ ∘ ((proj₁ fg) ⁂ K.₁ (proj₂ fg)) ≈ K.₁ ((proj₁ fg) ⁂ (proj₂ fg)) ∘ τ P₁
    commute' {(U , V)} {(W , X)} (f , g) = by-stability (algebras _) (η _ ∘ (f ⁂ g)) law₁ law₂ pres₁ pres₂
      where
      law₁ : η (W × X) ∘ (f ⁂ g) ≈ (τ (W , X) ∘ (f ⁂ K.₁ g)) ∘ (id ⁂ η V)
      law₁ = sym (begin 
        (τ (W , X) ∘ (f ⁂ K.₁ g)) ∘ (id ⁂ η V) ≈⟨ pullʳ ⁂∘⁂ ⟩ 
        τ (W , X) ∘ (f ∘ id ⁂ K.₁ g ∘ η V)     ≈⟨ refl⟩∘⟨ (⁂-cong₂ id-comm (K₁η g)) ⟩ 
        τ (W , X) ∘ (id ∘ f ⁂ η X ∘ g)         ≈⟨ refl⟩∘⟨ (sym ⁂∘⁂) ⟩ 
        τ (W , X) ∘ (id ⁂ η X) ∘ (f ⁂ g)       ≈⟨ pullˡ (τ-η (W , X)) ⟩ 
        η (W × X) ∘ (f ⁂ g)                     ∎)
      law₂ : η (W × X) ∘ (f ⁂ g) ≈ (K.₁ (f ⁂ g) ∘ τ (U , V)) ∘ (id ⁂ η V)
      law₂ = sym (begin
        (K.₁ (f ⁂ g) ∘ τ (U , V)) ∘ (id ⁂ η V) ≈⟨ pullʳ (τ-η (U , V)) ⟩ 
        K.₁ (f ⁂ g) ∘ η (U × V)                 ≈⟨ K₁η (f ⁂ g) ⟩ 
        η (W × X) ∘ (f ⁂ g)                     ∎)
      pres₁ : ∀ {Z : Obj} (h : Z ⇒ K.₀ V + Z) → (τ (W , X) ∘ (f ⁂ K.₁ g)) ∘ (id ⁂ h #) ≈ ((τ (W , X) ∘ (f ⁂ K.₁ g) +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ h))#
      pres₁ {Z} h = begin 
        (τ (W , X) ∘ (f ⁂ K.₁ g)) ∘ (id ⁂ h #)                                         ≈⟨ pullʳ ⁂∘⁂ ⟩ 
        τ (W , X) ∘ (f ∘ id ⁂ K.₁ g ∘ (h #))                                           ≈⟨ refl⟩∘⟨ (⁂-cong₂ id-comm ((Elgot-Algebra-Morphism.preserves (((freealgebras _) FreeObject.*) (η X ∘ g))) ○ sym identityʳ)) ⟩ 
        τ (W , X) ∘ (id ∘ f ⁂ ((K.₁ g +₁ id) ∘ h) # ∘ id)                            ≈⟨ refl⟩∘⟨ (sym ⁂∘⁂) ⟩ 
        τ (W , X) ∘ (id ⁂ ((K.₁ g +₁ id) ∘ h) #) ∘ (f ⁂ id)                          ≈⟨ pullˡ (♯-preserving (stable _) (η _) ((K.₁ g +₁ id) ∘ h)) ⟩ 
        ((τ (W , X) +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ (K.₁ g +₁ id) ∘ h)) # ∘ (f ⁂ id) ≈⟨ sym (#-Uniformity (algebras _) uni-helper) ⟩ 
        ((τ (W , X) ∘ (f ⁂ K.₁ g) +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ h))#                 ∎ 
        where
        uni-helper = begin 
          (id +₁ f ⁂ id) ∘ (τ (W , X) ∘ (f ⁂ K.₁ g) +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ h) ≈⟨ pullˡ +₁∘+₁ ⟩ 
          (id ∘ τ (W , X) ∘ (f ⁂ K.₁ g) +₁ (f ⁂ id) ∘ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ h)  ≈⟨ (+₁-cong₂ identityˡ id-comm) ⟩∘⟨refl ⟩ 
          (τ (W , X) ∘ (f ⁂ K.₁ g) +₁ id ∘ (f ⁂ id)) ∘ distributeˡ⁻¹ ∘ (id ⁂ h)        ≈⟨ (sym +₁∘+₁) ⟩∘⟨refl ⟩ 
          ((τ (W , X) +₁ id) ∘ ((f ⁂ K.₁ g) +₁ (f ⁂ id))) ∘ distributeˡ⁻¹ ∘ (id ⁂ h)   ≈⟨ pullʳ (pullˡ (distributeˡ⁻¹-natural f (K.₁ g) id)) ⟩ 
          (τ (W , X) +₁ id) ∘ (distributeˡ⁻¹ ∘ (f ⁂ (K.₁ g +₁ id))) ∘ (id ⁂ h)         ≈⟨ refl⟩∘⟨ (pullʳ (⁂∘⁂ ○ ⁂-cong₂ identityʳ refl)) ⟩ 
          (τ (W , X) +₁ id) ∘ distributeˡ⁻¹ ∘ (f ⁂ (K.₁ g +₁ id) ∘ h)                   ≈˘⟨ pullʳ (pullʳ (⁂∘⁂ ○ ⁂-cong₂ identityˡ identityʳ)) ⟩ 
          ((τ (W , X) +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ (K.₁ g +₁ id) ∘ h)) ∘ (f ⁂ id)   ∎
      pres₂ : ∀ {Z : Obj} (h : Z ⇒ K.₀ V + Z) → (K.₁ (f ⁂ g) ∘ τ (U , V)) ∘ (id ⁂ h #) ≈ ((K.₁ (f ⁂ g) ∘ τ (U , V) +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ h)) #
      pres₂ {Z} h = begin 
        (K.₁ (f ⁂ g) ∘ τ (U , V)) ∘ (id ⁂ (h #))                                 ≈⟨ pullʳ (τ-comm h) ⟩ 
        K.₁ (f ⁂ g) ∘ ((τ (U , V) +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ h)) #          ≈⟨ Elgot-Algebra-Morphism.preserves (((freealgebras _) FreeObject.*) (η (W × X) ∘ (f ⁂ g))) ⟩ 
        ((K.₁ (f ⁂ g) +₁ id) ∘ (τ (U , V) +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ h)) # ≈⟨ #-resp-≈ (algebras (W × X)) (pullˡ (+₁∘+₁ ○ +₁-cong₂ refl identity²)) ⟩ 
        ((K.₁ (f ⁂ g) ∘ τ (U , V) +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ h)) #          ∎
  Strength.identityˡ KStrength {X} = τ-π₂ (Terminal.⊤ terminal , X)

  Strength.η-comm KStrength {A} {B} = τ-η (A , B)

  Strength.μ-η-comm KStrength {A} {B} = by-stability (algebras _) (τ (A , B)) law₁ law₂ pres₁ pres₂
    where
    law₁ : τ (A , B) ≈ (μ.η _ ∘ K.₁ (τ _) ∘ τ _) ∘ (id ⁂ η _)
    law₁ = sym (begin 
      (μ.η _ ∘ K.₁ (τ _) ∘ τ _) ∘ (id ⁂ η _) ≈⟨ pullʳ (pullʳ (τ-η _)) ⟩ 
      μ.η _ ∘ K.₁ (τ _) ∘ η _                 ≈⟨ refl⟩∘⟨ (K₁η (τ (A , B))) ⟩ 
      μ.η _ ∘ η _ ∘ τ _                       ≈⟨ cancelˡ monadK.identityʳ ⟩ 
      τ _                                     ∎)
    law₂ : τ (A , B) ≈ (τ (A , B) ∘ (id ⁂ μ.η B)) ∘ (id ⁂ η (K.₀ B))
    law₂ = (sym (cancelʳ (⁂∘⁂ ○ ⁂-cong₂ identity² monadK.identityʳ ○ ⟨⟩-unique id-comm id-comm)))
    pres₁ : ∀ {Z : Obj} (h : Z ⇒ K.₀ (K.₀ B) + Z) → (μ.η _ ∘ K.₁ (τ _) ∘ τ _) ∘ (id ⁂ h #) ≈ ((μ.η _ ∘ K.₁ (τ (A , B)) ∘ τ _ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ h)) #
    pres₁ {Z} h = begin 
      (μ.η _ ∘ K.₁ (τ _) ∘ τ _) ∘ (id ⁂ h #)                                                      ≈⟨ pullʳ (pullʳ (τ-comm h)) ⟩ 
      μ.η _ ∘ K.₁ (τ _) ∘ (((τ (A , K.₀ B) +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ h)) #)                 ≈⟨ refl⟩∘⟨ (Elgot-Algebra-Morphism.preserves (((freealgebras _) FreeObject.*) (η _ ∘ τ _))) ⟩ 
      μ.η _ ∘ ((K.₁ (τ _) +₁ id) ∘ (τ (A , K.₀ B) +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ h)) #          ≈⟨ Elgot-Algebra-Morphism.preserves (((freealgebras _) FreeObject.*) id) ⟩ 
      ((μ.η _ +₁ id) ∘ (K.₁ (τ _) +₁ id) ∘ (τ (A , K.₀ B) +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ h)) # ≈⟨ #-resp-≈ (algebras _) (pullˡ +₁∘+₁) ⟩ 
      ((μ.η _ ∘ K.₁ (τ _) +₁ id ∘ id) ∘ (τ (A , K.₀ B) +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ h)) #    ≈⟨ #-resp-≈ (algebras _) (pullˡ +₁∘+₁) ⟩
      (((μ.η _ ∘ K.₁ (τ _)) ∘ τ _ +₁ (id ∘ id) ∘ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ h)) #             ≈⟨ #-resp-≈ (algebras _) ((+₁-cong₂ assoc (cancelʳ identity²)) ⟩∘⟨refl) ⟩
      ((μ.η _ ∘ K.₁ (τ (A , B)) ∘ τ _ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ h)) #                       ∎
    pres₂ : ∀ {Z : Obj} (h : Z ⇒ K.₀ (K.₀ B) + Z) → (τ _ ∘ (id ⁂ μ.η _)) ∘ (id ⁂ h #) ≈ ((τ _ ∘ (id ⁂ μ.η _) +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ h)) #
    pres₂ {Z} h = begin 
      (τ _ ∘ (id ⁂ μ.η _)) ∘ (id ⁂ h #)                                         ≈⟨ pullʳ ⁂∘⁂ ⟩ 
      τ _ ∘ (id ∘ id ⁂ μ.η _ ∘ h #)                                             ≈⟨ refl⟩∘⟨ (⁂-cong₂ identity² (Elgot-Algebra-Morphism.preserves (((freealgebras _) FreeObject.*) id))) ⟩ 
      τ _ ∘ (id ⁂ ((μ.η _ +₁ id) ∘ h) #)                                        ≈⟨ τ-comm ((μ.η B +₁ id) ∘ h) ⟩ 
      ((τ _ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ (μ.η B +₁ id) ∘ h)) #               ≈⟨ #-resp-≈ (algebras _) (refl⟩∘⟨ (refl⟩∘⟨ (⁂-cong₂ (sym identity²) refl ○ sym ⁂∘⁂))) ⟩ 
      ((τ _ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ (μ.η B +₁ id)) ∘ (id ⁂ h)) #       ≈⟨ #-resp-≈ (algebras _) (refl⟩∘⟨ (pullˡ (sym (distributeˡ⁻¹-natural id (μ.η B) id)))) ⟩
      ((τ _ +₁ id) ∘ ((id ⁂ μ.η B +₁ id ⁂ id) ∘ distributeˡ⁻¹) ∘ (id ⁂ h)) # ≈⟨ #-resp-≈ (algebras _) (pullˡ (pullˡ (+₁∘+₁ ○ +₁-cong₂ refl (elimʳ (⟨⟩-unique id-comm id-comm))))) ⟩ 
      (((τ _ ∘ (id ⁂ μ.η B) +₁ id) ∘ distributeˡ⁻¹) ∘ (id ⁂ h)) #              ≈⟨ #-resp-≈ (algebras _) assoc ⟩
      ((τ _ ∘ (id ⁂ μ.η _) +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ h)) #                ∎

  Strength.strength-assoc KStrength {X} {Y} {Z} = by-stability (algebras _) (η (X × Y × Z) ∘ assocˡ) law₁ law₂ pres₁ pres₂
    where
    law₁ : η (X × Y × Z) ∘ assocˡ ≈ (K.₁ assocˡ ∘ τ (X × Y , Z)) ∘ (id ⁂ η Z)
    law₁ = sym (pullʳ (τ-η _) ○ K₁η _)
    law₂ : η (X × Y × Z) ∘ assocˡ ≈ (τ _ ∘ (id ⁂ τ _) ∘ assocˡ) ∘ (id ⁂ η _)
    law₂ = sym (begin 
      (τ _ ∘ (id ⁂ τ _) ∘ assocˡ) ∘ (id ⁂ η _)                                       ≈⟨ (refl⟩∘⟨ ⁂∘⟨⟩) ⟩∘⟨refl ⟩ 
      (τ _ ∘ ⟨ id ∘ π₁ ∘ π₁ , τ _ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ (id ⁂ η _)                 ≈⟨ pullʳ ⟨⟩∘ ⟩ 
      τ _ ∘ ⟨ (id ∘ π₁ ∘ π₁) ∘ (id ⁂ η _) , (τ _ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩) ∘ (id ⁂ η _) ⟩ ≈⟨ refl⟩∘⟨ (⟨⟩-cong₂ (identityˡ ⟩∘⟨refl ○ pullʳ π₁∘⁂) (pullʳ ⟨⟩∘)) ⟩ 
      τ _ ∘ ⟨ π₁ ∘ id ∘ π₁ , τ _ ∘ ⟨ (π₂ ∘ π₁) ∘ (id ⁂ η _) , π₂ ∘ (id ⁂ η _) ⟩ ⟩   ≈⟨ refl⟩∘⟨ (⟨⟩-cong₂ (refl⟩∘⟨ identityˡ) (refl⟩∘⟨ (⟨⟩-cong₂ (pullʳ π₁∘⁂) π₂∘⁂))) ⟩ 
      τ _ ∘ ⟨ π₁ ∘ π₁ , τ _ ∘ ⟨ π₂ ∘ id ∘ π₁ , η _ ∘ π₂ ⟩ ⟩                           ≈⟨ refl⟩∘⟨ (⟨⟩-cong₂ (sym identityˡ) (refl⟩∘⟨ ((⟨⟩-cong₂ (sym identityˡ) refl) ○ sym ⁂∘⟨⟩))) ⟩ 
      τ _ ∘ ⟨ id ∘ π₁ ∘ π₁ , τ _ ∘ (id ⁂ η _) ∘ ⟨ π₂ ∘ id ∘ π₁ , π₂ ⟩ ⟩             ≈⟨ refl⟩∘⟨ (⟨⟩-cong₂ refl (pullˡ (τ-η (Y , Z)))) ⟩ 
      τ _ ∘ ⟨ id ∘ π₁ ∘ π₁ , η _ ∘ ⟨ π₂ ∘ id ∘ π₁ , π₂ ⟩ ⟩                           ≈⟨ refl⟩∘⟨ (sym ⁂∘⟨⟩) ⟩ 
      τ _ ∘ (id ⁂ η _) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ id ∘ π₁ , π₂ ⟩ ⟩                         ≈⟨ pullˡ (τ-η _) ⟩ 
      η _ ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ id ∘ π₁ , π₂ ⟩ ⟩                                       ≈⟨ refl⟩∘⟨ ⟨⟩-cong₂ refl (⟨⟩-cong₂ (refl⟩∘⟨ identityˡ) refl) ⟩ 
      η (X × Y × Z) ∘ assocˡ                                                           ∎)
    pres₁ : ∀ {A : Obj} (h : A ⇒ K.₀ Z + A) → (K.₁ assocˡ ∘ τ _) ∘ (id ⁂ h #) ≈ ((K.₁ assocˡ ∘ τ _ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ h)) #
    pres₁ {A} h = begin 
      (K.₁ assocˡ ∘ τ _) ∘ (id ⁂ h #)                                  ≈⟨ pullʳ (τ-comm h) ⟩ 
      K.₁ assocˡ ∘ ((τ _ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ h))#          ≈⟨ Elgot-Algebra-Morphism.preserves (((freealgebras _) FreeObject.*) _) ⟩ 
      ((K.₁ assocˡ +₁ id) ∘ (τ _ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ h))# ≈⟨ #-resp-≈ (algebras _) (pullˡ (+₁∘+₁ ○ +₁-cong₂ refl identity²)) ⟩ 
      ((K.₁ assocˡ ∘ τ _ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ h)) #         ∎
    pres₂ : ∀ {A : Obj} (h : A ⇒ K.₀ Z + A) → (τ _ ∘ (id ⁂ τ _) ∘ assocˡ) ∘ (id ⁂ h #) ≈ ((τ _ ∘ (id ⁂ τ _) ∘ assocˡ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ h)) #
    pres₂ {A} h = begin 
      (τ _ ∘ (id ⁂ τ _) ∘ assocˡ) ∘ (id ⁂ h #)                                                         ≈⟨ (refl⟩∘⟨ ⁂∘⟨⟩) ⟩∘⟨refl ⟩ 
      (τ _ ∘ ⟨ id ∘ π₁ ∘ π₁ , τ _ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ (id ⁂ h #)                                   ≈⟨ pullʳ ⟨⟩∘ ⟩ 
      τ _ ∘ ⟨ (id ∘ π₁ ∘ π₁) ∘ (id ⁂ h #) , (τ _ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩) ∘ (id ⁂ h #) ⟩                   ≈⟨ refl⟩∘⟨ (⟨⟩-cong₂ (identityˡ ⟩∘⟨refl ○ pullʳ π₁∘⁂) (pullʳ ⟨⟩∘)) ⟩ 
      τ _ ∘ ⟨ π₁ ∘ id ∘ π₁ , τ _ ∘ ⟨ (π₂ ∘ π₁) ∘ (id ⁂ h #) , π₂ ∘ (id ⁂ h #) ⟩ ⟩                     ≈⟨ refl⟩∘⟨ ⟨⟩-cong₂ (refl⟩∘⟨ identityˡ) (refl⟩∘⟨ (⟨⟩-cong₂ (pullʳ π₁∘⁂) π₂∘⁂)) ⟩ 
      τ _ ∘ ⟨ π₁ ∘ π₁ , τ _ ∘ ⟨ π₂ ∘ id ∘ π₁ , h # ∘ π₂ ⟩ ⟩                                             ≈⟨ refl⟩∘⟨ (⟨⟩-cong₂ refl (refl⟩∘⟨ (⟨⟩-cong₂ ((refl⟩∘⟨ identityˡ) ○ sym identityˡ) refl))) ⟩ 
      τ _ ∘ ⟨ π₁ ∘ π₁ , τ _ ∘ ⟨ id ∘ π₂ ∘ π₁ , h # ∘ π₂ ⟩ ⟩                                             ≈⟨ refl⟩∘⟨ ⟨⟩-cong₂ refl (refl⟩∘⟨ (sym ⁂∘⟨⟩)) ⟩ 
      τ _ ∘ ⟨ π₁ ∘ π₁ , τ _ ∘ (id ⁂ h #) ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩                                           ≈⟨ refl⟩∘⟨ (⟨⟩-cong₂ (sym identityˡ) (pullˡ (τ-comm h))) ⟩ 
      τ _ ∘ ⟨ id ∘ π₁ ∘ π₁ , (((τ (Y , Z) +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ h)) #) ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩  ≈⟨ refl⟩∘⟨ (sym ⁂∘⟨⟩) ⟩ 
      τ _ ∘ (id ⁂ ((τ (Y , Z) +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ h)) #) ∘ assocˡ                          ≈⟨ pullˡ (τ-comm _) ⟩ 
      ((τ _ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ (τ (Y , Z) +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ h))) # ∘ assocˡ ≈⟨ sym (#-Uniformity (algebras _) uni-helper) ⟩
      ((τ _ ∘ (id ⁂ τ _) ∘ assocˡ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ h)) #                                ∎
      where
        uni-helper : (id +₁ assocˡ) ∘ (τ _ ∘ (id ⁂ τ (Y , Z)) ∘ assocˡ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ h) ≈ ((τ _ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ (τ (Y , Z) +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ h))) ∘ assocˡ
        uni-helper = begin 
          (id +₁ assocˡ) ∘ (τ _ ∘ (id ⁂ τ (Y , Z)) ∘ assocˡ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ h)                           ≈⟨ pullˡ +₁∘+₁ ⟩ 
          (id ∘ τ _ ∘ (id ⁂ τ (Y , Z)) ∘ assocˡ +₁ assocˡ ∘ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ h)                              ≈⟨ (+₁-cong₂ identityˡ id-comm) ⟩∘⟨refl ⟩ 
          (τ _ ∘ (id ⁂ τ (Y , Z)) ∘ assocˡ +₁ id ∘ assocˡ) ∘ distributeˡ⁻¹ ∘ (id ⁂ h)                                    ≈˘⟨ (+₁∘+₁ ○ +₁-cong₂ assoc refl) ⟩∘⟨refl ⟩ 
          ((τ _ ∘ (id ⁂ τ (Y , Z)) +₁ id) ∘ (assocˡ +₁ assocˡ)) ∘ distributeˡ⁻¹ ∘ (id ⁂ h)                               ≈⟨ pullʳ (pullˡ (sym distributeˡ⁻¹-assoc)) ⟩ 
          (τ _ ∘ (id ⁂ τ (Y , Z)) +₁ id) ∘ (distributeˡ⁻¹ ∘ (id ⁂ distributeˡ⁻¹) ∘ assocˡ) ∘ (id ⁂ h)                   ≈⟨ refl⟩∘⟨ assoc²βε ⟩ 
          (τ _ ∘ (id ⁂ τ _) +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ distributeˡ⁻¹) ∘ assocˡ ∘ (id ⁂ h)                           ≈˘⟨ (+₁-cong₂ refl (elimʳ (⟨⟩-unique id-comm id-comm))) ⟩∘⟨refl ⟩ 
          (τ _ ∘ (id ⁂ τ _) +₁ id ∘ (id ⁂ id)) ∘ distributeˡ⁻¹ ∘ (id ⁂ distributeˡ⁻¹) ∘ assocˡ ∘ (id ⁂ h)             ≈˘⟨ assoc ○ assoc ⟩
          (((τ _ ∘ (id ⁂ τ _) +₁ id ∘ (id ⁂ id)) ∘ distributeˡ⁻¹) ∘ (id ⁂ distributeˡ⁻¹)) ∘ _≅_.to ×-assoc ∘ (id ⁂ h) ≈˘⟨ pullˡ (pullˡ (pullˡ +₁∘+₁)) ⟩
          (τ _ +₁ id) ∘ ((((id ⁂ τ _) +₁ (id ⁂ id)) ∘ distributeˡ⁻¹) ∘ (id ⁂ distributeˡ⁻¹)) ∘ assocˡ ∘ (id ⁂ h)      ≈⟨ refl⟩∘⟨ ((distributeˡ⁻¹-natural id (τ (Y , Z)) id) ⟩∘⟨refl) ⟩∘⟨refl ⟩ 
          (τ _ +₁ id) ∘ ((distributeˡ⁻¹ ∘ (id ⁂ (τ (Y , Z) +₁ id))) ∘ (id ⁂ distributeˡ⁻¹)) ∘ assocˡ ∘ (id ⁂ h)        ≈⟨ refl⟩∘⟨ (assoc ○ assoc ○ refl⟩∘⟨ sym-assoc) ⟩
          (τ _ +₁ id) ∘ distributeˡ⁻¹ ∘ ((id ⁂ (τ (Y , Z) +₁ id)) ∘ (id ⁂ distributeˡ⁻¹)) ∘ assocˡ ∘ (id ⁂ h)          ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (⁂∘⁂ ○ ⁂-cong₂ identity² refl) ⟩∘⟨refl ⟩ 
          (τ _ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ (τ (Y , Z) +₁ id) ∘ distributeˡ⁻¹) ∘ assocˡ ∘ (id ⁂ h)                    ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ ⁂-cong₂ (sym (⟨⟩-unique id-comm id-comm)) refl ⟩ 
          (τ _ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ (τ (Y , Z) +₁ id) ∘ distributeˡ⁻¹) ∘ assocˡ ∘ ((id ⁂ id) ⁂ h)            ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ assocˡ∘⁂ ⟩ 
          (τ _ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ (τ (Y , Z) +₁ id) ∘ distributeˡ⁻¹) ∘ (id ⁂ (id ⁂ h)) ∘ assocˡ            ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ assoc ⟩
          (τ _ +₁ id) ∘ distributeˡ⁻¹ ∘ ((id ⁂ (τ (Y , Z) +₁ id) ∘ distributeˡ⁻¹) ∘ (id ⁂ (id ⁂ h))) ∘ assocˡ          ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⁂∘⁂ ⟩∘⟨refl ⟩ 
          (τ _ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ∘ id ⁂ ((τ (Y , Z) +₁ id) ∘ distributeˡ⁻¹) ∘ (id ⁂ h)) ∘ assocˡ            ≈⟨ refl⟩∘⟨ (refl⟩∘⟨ ((⁂-cong₂ identity² assoc) ⟩∘⟨refl) ○ sym-assoc) ○ sym-assoc ⟩
          ((τ _ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ (τ (Y , Z) +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ h))) ∘ assocˡ                  ∎

  KStrong : StrongMonad {C = C} monoidal
  KStrong = record 
    { M = monadK
    ; strength = KStrength
    }

  module strongK = StrongMonad KStrong

  τ-comm-id : ∀ {X Y Z} (f : X ⇒ Y) → τ (Y , Z) ∘ (f ⁂ id) ≈ K.₁ (f ⁂ id) ∘ τ (X , Z)
  τ-comm-id {X} {Y} {Z} f = begin 
    τ (Y , Z) ∘ (f ⁂ id)     ≈⟨ refl⟩∘⟨ (⁂-cong₂ refl (sym K.identity)) ⟩ 
    τ (Y , Z) ∘ (f ⁂ K.₁ id) ≈⟨ strengthen.commute (f , id) ⟩ 
    K.₁ (f ⁂ id) ∘ τ (X , Z) ∎
    where open strongK using (strengthen)

  τ-kleisli-assoc : ∀ {X Y Z U} (f : X ⇒ K.₀ Y) (g : Z ⇒ K.₀ U) → extend (τ _ ∘ (id ⁂ g)) ∘ τ _ ∘ (extend f ⁂ id) ≈ τ _ ∘ (extend f ⁂ extend g)
  τ-kleisli-assoc {X} {Y} {Z} {U} f g = begin 
    extend (τ _ ∘ (id ⁂ g)) ∘ τ _ ∘ (extend f ⁂ id)        ≈˘⟨ pullˡ (extend∘F₁ monadK (τ _) (id ⁂ g)) ⟩ 
    extend (τ _) ∘ K.₁ (id ⁂ g) ∘ τ _ ∘ (extend f ⁂ id)    ≈⟨ refl⟩∘⟨ (pullˡ (sym (strengthen.commute (id , g))) ○ assoc) ⟩ 
    extend (τ _) ∘ τ _ ∘ (id ⁂ K.₁ g) ∘ (extend f ⁂ id)    ≈⟨ pullˡ (assoc ○ strongK.μ-η-comm) ⟩ 
    (τ _ ∘ (id ⁂ μ.η _)) ∘ (id ⁂ K.₁ g) ∘ (extend f ⁂ id) ≈⟨ pullʳ (pullˡ (⁂∘⁂ ○ ⁂-cong₂ identity² refl)) ⟩
    τ _ ∘ (id ⁂ extend g) ∘ (extend f ⁂ id)                ≈⟨ refl⟩∘⟨ (⁂∘⁂ ○ ⁂-cong₂ identityˡ identityʳ) ⟩ 
    τ _ ∘ (extend f ⁂ extend g)                              ∎
    where open strongK using (strengthen)