K is a Strong Monad

module Monad.Instance.K.Strong {o ℓ e} (ambient : Ambient o ℓ e) (MK : MIK.MonadK ambient) where
  open Ambient ambient
  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 ambient
  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)

K is a strong monad with the strength defined as η ♯, where ♯ is the operator we get from stability. We will proof the strength laws ‘by stability’ i.e. by using the uniqueness of the stability operator.

First the definition of τ and some facts:

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

    τ-η : τ ∘ (idC ⁂ η 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.₁ π₂ ∘ τ) ∘ (idC ⁂ η _)
      comm₁ = sym (begin 
        (K.₁ π₂ ∘ τ) ∘ (idC ⁂ η _) ≈⟨ pullʳ τ-η ⟩ 
        K.₁ π₂ ∘ η _                 ≈⟨ (sym (F₁⇒extend monadK π₂)) ⟩∘⟨refl ⟩
        extend (η _ ∘ π₂) ∘ η _                              ≈⟨ kleisliK.identityʳ ⟩
        η _ ∘ π₂                                             ∎)
      comm₂ : ∀ {Z : Obj} (h : Z ⇒ K.₀ Y + Z) → (K.₁ π₂ ∘ τ) ∘ (idC ⁂ h # ) ≈ ((K.₁ π₂ ∘ τ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))#
      comm₂ {Z} h = begin
        (K.₁ π₂ ∘ τ) ∘ (idC ⁂ h #)                                   ≈⟨ pullʳ (♯-preserving (stable Y) (η _) h) ⟩ 
        K.₁ π₂ ∘ ((τ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #          ≈⟨ Elgot-Algebra-Morphism.preserves ((freealgebras (X × Y) FreeObject.*) (η _ ∘ π₂)) ⟩
        ((K.₁ π₂ +₁ idC) ∘ (τ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈⟨ #-resp-≈ (algebras Y) (pullˡ (+₁∘+₁ ○ +₁-cong₂ refl identity²)) ⟩
        ((K.₁ π₂ ∘ τ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))#           ∎
      comm₃ : ∀ {Z : Obj} (h : Z ⇒ K.₀ Y + Z) → π₂ ∘ (idC ⁂ h #) ≈ ((π₂ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #
      comm₃ {Z} h = begin 
        π₂ ∘ (idC ⁂ h #)                            ≈⟨ π₂∘⁂ ⟩ 
        h # ∘ π₂                                    ≈⟨ sym (#-Uniformity (algebras Y) uni-helper) ⟩ 
        ((π₂ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ∎
        where
        uni-helper = begin 
          (idC +₁ π₂) ∘ (π₂ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ≈⟨ pullˡ +₁∘+₁ ⟩ 
          (idC ∘ π₂ +₁ π₂ ∘ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)    ≈⟨ (+₁-cong₂ identityˡ identityʳ) ⟩∘⟨refl ⟩ 
          (π₂ +₁ π₂) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)                ≈⟨ pullˡ distributeˡ⁻¹-π₂ ⟩ 
          π₂ ∘ (idC ⁂ h)                                        ≈⟨ project₂ ⟩ 
          h ∘ π₂                                                ∎

  τ-comm : ∀ {X Y Z : Obj} (h : Z ⇒ K.₀ Y + Z) → τ (X , Y) ∘ (idC ⁂ h #) ≈ ((τ (X , Y) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ 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                ∎

Now the strength proofs:

  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)) ∘ (idC ⁂ η V)
      law₁ = sym (begin 
        (τ (W , X) ∘ (f ⁂ K.₁ g)) ∘ (idC ⁂ η V) ≈⟨ pullʳ ⁂∘⁂ ⟩ 
        τ (W , X) ∘ (f ∘ idC ⁂ K.₁ g ∘ η V)     ≈⟨ refl⟩∘⟨ (⁂-cong₂ id-comm (K₁η g)) ⟩ 
        τ (W , X) ∘ (idC ∘ f ⁂ η X ∘ g)         ≈⟨ refl⟩∘⟨ (sym ⁂∘⁂) ⟩ 
        τ (W , X) ∘ (idC ⁂ η X) ∘ (f ⁂ g)       ≈⟨ pullˡ (τ-η (W , X)) ⟩ 
        η (W × X) ∘ (f ⁂ g)                     ∎)
      law₂ : η (W × X) ∘ (f ⁂ g) ≈ (K.₁ (f ⁂ g) ∘ τ (U , V)) ∘ (idC ⁂ η V)
      law₂ = sym (begin
        (K.₁ (f ⁂ g) ∘ τ (U , V)) ∘ (idC ⁂ η 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)) ∘ (idC ⁂ h #) ≈ ((τ (W , X) ∘ (f ⁂ K.₁ g) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))#
      pres₁ {Z} h = begin 
        (τ (W , X) ∘ (f ⁂ K.₁ g)) ∘ (idC ⁂ h #)                                         ≈⟨ pullʳ ⁂∘⁂ ⟩ 
        τ (W , X) ∘ (f ∘ idC ⁂ K.₁ g ∘ (h #))                                           ≈⟨ refl⟩∘⟨ (⁂-cong₂ id-comm ((Elgot-Algebra-Morphism.preserves (((freealgebras _) FreeObject.*) (η X ∘ g))) ○ sym identityʳ)) ⟩ 
        τ (W , X) ∘ (idC ∘ f ⁂ ((K.₁ g +₁ idC) ∘ h) # ∘ idC)                            ≈⟨ refl⟩∘⟨ (sym ⁂∘⁂) ⟩ 
        τ (W , X) ∘ (idC ⁂ ((K.₁ g +₁ idC) ∘ h) #) ∘ (f ⁂ idC)                          ≈⟨ pullˡ (♯-preserving (stable _) (η _) ((K.₁ g +₁ idC) ∘ h)) ⟩ 
        ((τ (W , X) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ (K.₁ g +₁ idC) ∘ h)) # ∘ (f ⁂ idC) ≈⟨ sym (#-Uniformity (algebras _) uni-helper) ⟩ 
        ((τ (W , X) ∘ (f ⁂ K.₁ g) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))#                 ∎ 
        where
        uni-helper = begin 
          (idC +₁ f ⁂ idC) ∘ (τ (W , X) ∘ (f ⁂ K.₁ g) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ≈⟨ pullˡ +₁∘+₁ ⟩ 
          (idC ∘ τ (W , X) ∘ (f ⁂ K.₁ g) +₁ (f ⁂ idC) ∘ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)  ≈⟨ (+₁-cong₂ identityˡ id-comm) ⟩∘⟨refl ⟩ 
          (τ (W , X) ∘ (f ⁂ K.₁ g) +₁ idC ∘ (f ⁂ idC)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)        ≈⟨ (sym +₁∘+₁) ⟩∘⟨refl ⟩ 
          ((τ (W , X) +₁ idC) ∘ ((f ⁂ K.₁ g) +₁ (f ⁂ idC))) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)   ≈⟨ pullʳ (pullˡ (distributeˡ⁻¹-natural f (K.₁ g) idC)) ⟩ 
          (τ (W , X) +₁ idC) ∘ (distributeˡ⁻¹ ∘ (f ⁂ (K.₁ g +₁ idC))) ∘ (idC ⁂ h)         ≈⟨ refl⟩∘⟨ (pullʳ (⁂∘⁂ ○ ⁂-cong₂ identityʳ refl)) ⟩ 
          (τ (W , X) +₁ idC) ∘ distributeˡ⁻¹ ∘ (f ⁂ (K.₁ g +₁ idC) ∘ h)                   ≈˘⟨ pullʳ (pullʳ (⁂∘⁂ ○ ⁂-cong₂ identityˡ identityʳ)) ⟩ 
          ((τ (W , X) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ (K.₁ g +₁ idC) ∘ h)) ∘ (f ⁂ idC)   ∎
      pres₂ : ∀ {Z : Obj} (h : Z ⇒ K.₀ V + Z) → (K.₁ (f ⁂ g) ∘ τ (U , V)) ∘ (idC ⁂ h #) ≈ ((K.₁ (f ⁂ g) ∘ τ (U , V) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #
      pres₂ {Z} h = begin 
        (K.₁ (f ⁂ g) ∘ τ (U , V)) ∘ (idC ⁂ (h #))                                 ≈⟨ pullʳ (τ-comm h) ⟩ 
        K.₁ (f ⁂ g) ∘ ((τ (U , V) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #          ≈⟨ Elgot-Algebra-Morphism.preserves (((freealgebras _) FreeObject.*) (η (W × X) ∘ (f ⁂ g))) ⟩ 
        ((K.₁ (f ⁂ g) +₁ idC) ∘ (τ (U , V) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈⟨ #-resp-≈ (algebras (W × X)) (pullˡ (+₁∘+₁ ○ +₁-cong₂ refl identity²)) ⟩ 
        ((K.₁ (f ⁂ g) ∘ τ (U , V) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ 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.₁ (τ _) ∘ τ _) ∘ (idC ⁂ η _)
    law₁ = sym (begin 
      (μ.η _ ∘ K.₁ (τ _) ∘ τ _) ∘ (idC ⁂ η _) ≈⟨ pullʳ (pullʳ (τ-η _)) ⟩ 
      μ.η _ ∘ K.₁ (τ _) ∘ η _                 ≈⟨ refl⟩∘⟨ (K₁η (τ (A , B))) ⟩ 
      μ.η _ ∘ η _ ∘ τ _                       ≈⟨ cancelˡ monadK.identityʳ ⟩ 
      τ _                                     ∎)
    law₂ : τ (A , B) ≈ (τ (A , B) ∘ (idC ⁂ μ.η B)) ∘ (idC ⁂ η (K.₀ B))
    law₂ = (sym (cancelʳ (⁂∘⁂ ○ ⁂-cong₂ identity² monadK.identityʳ ○ ⟨⟩-unique id-comm id-comm)))
    pres₁ : ∀ {Z : Obj} (h : Z ⇒ K.₀ (K.₀ B) + Z) → (μ.η _ ∘ K.₁ (τ _) ∘ τ _) ∘ (idC ⁂ h #) ≈ ((μ.η _ ∘ K.₁ (τ (A , B)) ∘ τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #
    pres₁ {Z} h = begin 
      (μ.η _ ∘ K.₁ (τ _) ∘ τ _) ∘ (idC ⁂ h #)                                                      ≈⟨ pullʳ (pullʳ (τ-comm h)) ⟩ 
      μ.η _ ∘ K.₁ (τ _) ∘ (((τ (A , K.₀ B) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #)                 ≈⟨ refl⟩∘⟨ (Elgot-Algebra-Morphism.preserves (((freealgebras _) FreeObject.*) (η _ ∘ τ _))) ⟩ 
      μ.η _ ∘ ((K.₁ (τ _) +₁ idC) ∘ (τ (A , K.₀ B) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #          ≈⟨ Elgot-Algebra-Morphism.preserves (((freealgebras _) FreeObject.*) idC) ⟩ 
      ((μ.η _ +₁ idC) ∘ (K.₁ (τ _) +₁ idC) ∘ (τ (A , K.₀ B) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈⟨ #-resp-≈ (algebras _) (pullˡ +₁∘+₁) ⟩ 
      ((μ.η _ ∘ K.₁ (τ _) +₁ idC ∘ idC) ∘ (τ (A , K.₀ B) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #    ≈⟨ #-resp-≈ (algebras _) (pullˡ +₁∘+₁) ⟩
      (((μ.η _ ∘ K.₁ (τ _)) ∘ τ _ +₁ (idC ∘ idC) ∘ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #             ≈⟨ #-resp-≈ (algebras _) ((+₁-cong₂ assoc (cancelʳ identity²)) ⟩∘⟨refl) ⟩
      ((μ.η _ ∘ K.₁ (τ (A , B)) ∘ τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #                       ∎
    pres₂ : ∀ {Z : Obj} (h : Z ⇒ K.₀ (K.₀ B) + Z) → (τ _ ∘ (idC ⁂ μ.η _)) ∘ (idC ⁂ h #) ≈ ((τ _ ∘ (idC ⁂ μ.η _) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #
    pres₂ {Z} h = begin 
      (τ _ ∘ (idC ⁂ μ.η _)) ∘ (idC ⁂ h #)                                         ≈⟨ pullʳ ⁂∘⁂ ⟩ 
      τ _ ∘ (idC ∘ idC ⁂ μ.η _ ∘ h #)                                             ≈⟨ refl⟩∘⟨ (⁂-cong₂ identity² (Elgot-Algebra-Morphism.preserves (((freealgebras _) FreeObject.*) idC))) ⟩ 
      τ _ ∘ (idC ⁂ ((μ.η _ +₁ idC) ∘ h) #)                                        ≈⟨ τ-comm ((μ.η B +₁ idC) ∘ h) ⟩ 
      ((τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ (μ.η B +₁ idC) ∘ h)) #               ≈⟨ #-resp-≈ (algebras _) (refl⟩∘⟨ (refl⟩∘⟨ (⁂-cong₂ (sym identity²) refl ○ sym ⁂∘⁂))) ⟩ 
      ((τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ (μ.η B +₁ idC)) ∘ (idC ⁂ h)) #       ≈⟨ #-resp-≈ (algebras _) (refl⟩∘⟨ (pullˡ (sym (distributeˡ⁻¹-natural idC (μ.η B) idC)))) ⟩
      ((τ _ +₁ idC) ∘ ((idC ⁂ μ.η B +₁ idC ⁂ idC) ∘ distributeˡ⁻¹) ∘ (idC ⁂ h)) # ≈⟨ #-resp-≈ (algebras _) (pullˡ (pullˡ (+₁∘+₁ ○ +₁-cong₂ refl (elimʳ (⟨⟩-unique id-comm id-comm))))) ⟩ 
      (((τ _ ∘ (idC ⁂ μ.η B) +₁ idC) ∘ distributeˡ⁻¹) ∘ (idC ⁂ h)) #              ≈⟨ #-resp-≈ (algebras _) assoc ⟩
      ((τ _ ∘ (idC ⁂ μ.η _) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ 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)) ∘ (idC ⁂ η Z)
    law₁ = sym (pullʳ (τ-η _) ○ K₁η _)
    law₂ : η (X × Y × Z) ∘ assocˡ ≈ (τ _ ∘ (idC ⁂ τ _) ∘ assocˡ) ∘ (idC ⁂ η _)
    law₂ = sym (begin 
      (τ _ ∘ (idC ⁂ τ _) ∘ assocˡ) ∘ (idC ⁂ η _)                                       ≈⟨ (refl⟩∘⟨ ⁂∘⟨⟩) ⟩∘⟨refl ⟩ 
      (τ _ ∘ ⟨ idC ∘ π₁ ∘ π₁ , τ _ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ (idC ⁂ η _)                 ≈⟨ pullʳ ⟨⟩∘ ⟩ 
      τ _ ∘ ⟨ (idC ∘ π₁ ∘ π₁) ∘ (idC ⁂ η _) , (τ _ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩) ∘ (idC ⁂ η _) ⟩ ≈⟨ refl⟩∘⟨ (⟨⟩-cong₂ (identityˡ ⟩∘⟨refl ○ pullʳ π₁∘⁂) (pullʳ ⟨⟩∘)) ⟩ 
      τ _ ∘ ⟨ π₁ ∘ idC ∘ π₁ , τ _ ∘ ⟨ (π₂ ∘ π₁) ∘ (idC ⁂ η _) , π₂ ∘ (idC ⁂ η _) ⟩ ⟩   ≈⟨ refl⟩∘⟨ (⟨⟩-cong₂ (refl⟩∘⟨ identityˡ) (refl⟩∘⟨ (⟨⟩-cong₂ (pullʳ π₁∘⁂) π₂∘⁂))) ⟩ 
      τ _ ∘ ⟨ π₁ ∘ π₁ , τ _ ∘ ⟨ π₂ ∘ idC ∘ π₁ , η _ ∘ π₂ ⟩ ⟩                           ≈⟨ refl⟩∘⟨ (⟨⟩-cong₂ (sym identityˡ) (refl⟩∘⟨ ((⟨⟩-cong₂ (sym identityˡ) refl) ○ sym ⁂∘⟨⟩))) ⟩ 
      τ _ ∘ ⟨ idC ∘ π₁ ∘ π₁ , τ _ ∘ (idC ⁂ η _) ∘ ⟨ π₂ ∘ idC ∘ π₁ , π₂ ⟩ ⟩             ≈⟨ refl⟩∘⟨ (⟨⟩-cong₂ refl (pullˡ (τ-η (Y , Z)))) ⟩ 
      τ _ ∘ ⟨ idC ∘ π₁ ∘ π₁ , η _ ∘ ⟨ π₂ ∘ idC ∘ π₁ , π₂ ⟩ ⟩                           ≈⟨ refl⟩∘⟨ (sym ⁂∘⟨⟩) ⟩ 
      τ _ ∘ (idC ⁂ η _) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ idC ∘ π₁ , π₂ ⟩ ⟩                         ≈⟨ pullˡ (τ-η _) ⟩ 
      η _ ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ idC ∘ π₁ , π₂ ⟩ ⟩                                       ≈⟨ refl⟩∘⟨ ⟨⟩-cong₂ refl (⟨⟩-cong₂ (refl⟩∘⟨ identityˡ) refl) ⟩ 
      η (X × Y × Z) ∘ assocˡ                                                           ∎)
    pres₁ : ∀ {A : Obj} (h : A ⇒ K.₀ Z + A) → (K.₁ assocˡ ∘ τ _) ∘ (idC ⁂ h #) ≈ ((K.₁ assocˡ ∘ τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #
    pres₁ {A} h = begin 
      (K.₁ assocˡ ∘ τ _) ∘ (idC ⁂ h #)                                  ≈⟨ pullʳ (τ-comm h) ⟩ 
      K.₁ assocˡ ∘ ((τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))#          ≈⟨ Elgot-Algebra-Morphism.preserves (((freealgebras _) FreeObject.*) _) ⟩ 
      ((K.₁ assocˡ +₁ idC) ∘ (τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# ≈⟨ #-resp-≈ (algebras _) (pullˡ (+₁∘+₁ ○ +₁-cong₂ refl identity²)) ⟩ 
      ((K.₁ assocˡ ∘ τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #         ∎
    pres₂ : ∀ {A : Obj} (h : A ⇒ K.₀ Z + A) → (τ _ ∘ (idC ⁂ τ _) ∘ assocˡ) ∘ (idC ⁂ h #) ≈ ((τ _ ∘ (idC ⁂ τ _) ∘ assocˡ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #
    pres₂ {A} h = begin 
      (τ _ ∘ (idC ⁂ τ _) ∘ assocˡ) ∘ (idC ⁂ h #)                                                         ≈⟨ (refl⟩∘⟨ ⁂∘⟨⟩) ⟩∘⟨refl ⟩ 
      (τ _ ∘ ⟨ idC ∘ π₁ ∘ π₁ , τ _ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ (idC ⁂ h #)                                   ≈⟨ pullʳ ⟨⟩∘ ⟩ 
      τ _ ∘ ⟨ (idC ∘ π₁ ∘ π₁) ∘ (idC ⁂ h #) , (τ _ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩) ∘ (idC ⁂ h #) ⟩                   ≈⟨ refl⟩∘⟨ (⟨⟩-cong₂ (identityˡ ⟩∘⟨refl ○ pullʳ π₁∘⁂) (pullʳ ⟨⟩∘)) ⟩ 
      τ _ ∘ ⟨ π₁ ∘ idC ∘ π₁ , τ _ ∘ ⟨ (π₂ ∘ π₁) ∘ (idC ⁂ h #) , π₂ ∘ (idC ⁂ h #) ⟩ ⟩                     ≈⟨ refl⟩∘⟨ ⟨⟩-cong₂ (refl⟩∘⟨ identityˡ) (refl⟩∘⟨ (⟨⟩-cong₂ (pullʳ π₁∘⁂) π₂∘⁂)) ⟩ 
      τ _ ∘ ⟨ π₁ ∘ π₁ , τ _ ∘ ⟨ π₂ ∘ idC ∘ π₁ , h # ∘ π₂ ⟩ ⟩                                             ≈⟨ refl⟩∘⟨ (⟨⟩-cong₂ refl (refl⟩∘⟨ (⟨⟩-cong₂ ((refl⟩∘⟨ identityˡ) ○ sym identityˡ) refl))) ⟩ 
      τ _ ∘ ⟨ π₁ ∘ π₁ , τ _ ∘ ⟨ idC ∘ π₂ ∘ π₁ , h # ∘ π₂ ⟩ ⟩                                             ≈⟨ refl⟩∘⟨ ⟨⟩-cong₂ refl (refl⟩∘⟨ (sym ⁂∘⟨⟩)) ⟩ 
      τ _ ∘ ⟨ π₁ ∘ π₁ , τ _ ∘ (idC ⁂ h #) ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩                                           ≈⟨ refl⟩∘⟨ (⟨⟩-cong₂ (sym identityˡ) (pullˡ (τ-comm h))) ⟩ 
      τ _ ∘ ⟨ idC ∘ π₁ ∘ π₁ , (((τ (Y , Z) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #) ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩  ≈⟨ refl⟩∘⟨ (sym ⁂∘⟨⟩) ⟩ 
      τ _ ∘ (idC ⁂ ((τ (Y , Z) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #) ∘ assocˡ                          ≈⟨ pullˡ (τ-comm _) ⟩ 
      ((τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ (τ (Y , Z) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))) # ∘ assocˡ ≈⟨ sym (#-Uniformity (algebras _) uni-helper) ⟩
      ((τ _ ∘ (idC ⁂ τ _) ∘ assocˡ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #                                ∎
      where
        uni-helper : (idC +₁ assocˡ) ∘ (τ _ ∘ (idC ⁂ τ (Y , Z)) ∘ assocˡ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ≈ ((τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ (τ (Y , Z) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))) ∘ assocˡ
        uni-helper = begin 
          (idC +₁ assocˡ) ∘ (τ _ ∘ (idC ⁂ τ (Y , Z)) ∘ assocˡ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)                           ≈⟨ pullˡ +₁∘+₁ ⟩ 
          (idC ∘ τ _ ∘ (idC ⁂ τ (Y , Z)) ∘ assocˡ +₁ assocˡ ∘ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)                              ≈⟨ (+₁-cong₂ identityˡ id-comm) ⟩∘⟨refl ⟩ 
          (τ _ ∘ (idC ⁂ τ (Y , Z)) ∘ assocˡ +₁ idC ∘ assocˡ) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)                                    ≈˘⟨ (+₁∘+₁ ○ +₁-cong₂ assoc refl) ⟩∘⟨refl ⟩ 
          ((τ _ ∘ (idC ⁂ τ (Y , Z)) +₁ idC) ∘ (assocˡ +₁ assocˡ)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)                               ≈⟨ pullʳ (pullˡ (sym distributeˡ⁻¹-assoc)) ⟩ 
          (τ _ ∘ (idC ⁂ τ (Y , Z)) +₁ idC) ∘ (distributeˡ⁻¹ ∘ (idC ⁂ distributeˡ⁻¹) ∘ assocˡ) ∘ (idC ⁂ h)                   ≈⟨ refl⟩∘⟨ assoc²' ⟩ 
          (τ _ ∘ (idC ⁂ τ _) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ distributeˡ⁻¹) ∘ assocˡ ∘ (idC ⁂ h)                           ≈˘⟨ (+₁-cong₂ refl (elimʳ (⟨⟩-unique id-comm id-comm))) ⟩∘⟨refl ⟩ 
          (τ _ ∘ (idC ⁂ τ _) +₁ idC ∘ (idC ⁂ idC)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ distributeˡ⁻¹) ∘ assocˡ ∘ (idC ⁂ h)             ≈˘⟨ assoc ○ assoc ⟩
          (((τ _ ∘ (idC ⁂ τ _) +₁ idC ∘ (idC ⁂ idC)) ∘ distributeˡ⁻¹) ∘ (idC ⁂ distributeˡ⁻¹)) ∘ _≅_.to ×-assoc ∘ (idC ⁂ h) ≈˘⟨ pullˡ (pullˡ (pullˡ +₁∘+₁)) ⟩
          (τ _ +₁ idC) ∘ ((((idC ⁂ τ _) +₁ (idC ⁂ idC)) ∘ distributeˡ⁻¹) ∘ (idC ⁂ distributeˡ⁻¹)) ∘ assocˡ ∘ (idC ⁂ h)      ≈⟨ refl⟩∘⟨ ((distributeˡ⁻¹-natural idC (τ (Y , Z)) idC) ⟩∘⟨refl) ⟩∘⟨refl ⟩ 
          (τ _ +₁ idC) ∘ ((distributeˡ⁻¹ ∘ (idC ⁂ (τ (Y , Z) +₁ idC))) ∘ (idC ⁂ distributeˡ⁻¹)) ∘ assocˡ ∘ (idC ⁂ h)        ≈⟨ refl⟩∘⟨ (assoc ○ assoc ○ refl⟩∘⟨ sym-assoc) ⟩
          (τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ ((idC ⁂ (τ (Y , Z) +₁ idC)) ∘ (idC ⁂ distributeˡ⁻¹)) ∘ assocˡ ∘ (idC ⁂ h)          ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (⁂∘⁂ ○ ⁂-cong₂ identity² refl) ⟩∘⟨refl ⟩ 
          (τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ (τ (Y , Z) +₁ idC) ∘ distributeˡ⁻¹) ∘ assocˡ ∘ (idC ⁂ h)                    ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ ⁂-cong₂ (sym (⟨⟩-unique id-comm id-comm)) refl ⟩ 
          (τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ (τ (Y , Z) +₁ idC) ∘ distributeˡ⁻¹) ∘ assocˡ ∘ ((idC ⁂ idC) ⁂ h)            ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ assocˡ∘⁂ ⟩ 
          (τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ (τ (Y , Z) +₁ idC) ∘ distributeˡ⁻¹) ∘ (idC ⁂ (idC ⁂ h)) ∘ assocˡ            ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ assoc ⟩
          (τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ ((idC ⁂ (τ (Y , Z) +₁ idC) ∘ distributeˡ⁻¹) ∘ (idC ⁂ (idC ⁂ h))) ∘ assocˡ          ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⁂∘⁂ ⟩∘⟨refl ⟩ 
          (τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ∘ idC ⁂ ((τ (Y , Z) +₁ idC) ∘ distributeˡ⁻¹) ∘ (idC ⁂ h)) ∘ assocˡ            ≈⟨ refl⟩∘⟨ (refl⟩∘⟨ ((⁂-cong₂ identity² assoc) ⟩∘⟨refl) ○ sym-assoc) ○ sym-assoc ⟩
          ((τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ (τ (Y , Z) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))) ∘ assocˡ                  ∎

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

  module strongK = StrongMonad KStrong

Two small lemmas about strength:

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

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