🚧 Work on commutativity of K

.envrc

@@ -0,0 +1 @@
+use flake

.gitignore

@@ -3,3 +3,4 @@
 *.log
 Everything.agda
 public/
+.direnv

README.md

@@ -24,3 +24,18 @@ So far the contributions are:
 
 ## TODO
 TODOs are found inside the literate agda files!
+
+## Usage
+The project requires a new version of agda-categories (newer than some package managers ship), so the easiest way to use this project is via the provided nix flake, which fetches my fork of agda-categories that is guaranteed to work with this project.
+
+To use the project you just have to open a development shell:
+```sh
+nix develop .
+```
+(this will take 20 - 30 minutes the first time, because it has to typecheck the agda-categories library)
+
+There is also a Makefile for compiling every module and generating the html documentation.
+
+```
+make
+```

flake.lock

@@ -0,0 +1,61 @@
+{
+  "nodes": {
+    "flake-utils": {
+      "inputs": {
+        "systems": "systems"
+      },
+      "locked": {
+        "lastModified": 1694529238,
+        "narHash": "sha256-zsNZZGTGnMOf9YpHKJqMSsa0dXbfmxeoJ7xHlrt+xmY=",
+        "owner": "numtide",
+        "repo": "flake-utils",
+        "rev": "ff7b65b44d01cf9ba6a71320833626af21126384",
+        "type": "github"
+      },
+      "original": {
+        "owner": "numtide",
+        "repo": "flake-utils",
+        "type": "github"
+      }
+    },
+    "nixpkgs": {
+      "locked": {
+        "lastModified": 1698288402,
+        "narHash": "sha256-jIIjApPdm+4yt8PglX8pUOexAdEiAax/DXW3S/Mb21E=",
+        "owner": "NixOS",
+        "repo": "nixpkgs",
+        "rev": "60b9db998f71ea49e1a9c41824d09aa274be1344",
+        "type": "github"
+      },
+      "original": {
+        "owner": "NixOS",
+        "ref": "nixos-23.05",
+        "repo": "nixpkgs",
+        "type": "github"
+      }
+    },
+    "root": {
+      "inputs": {
+        "flake-utils": "flake-utils",
+        "nixpkgs": "nixpkgs"
+      }
+    },
+    "systems": {
+      "locked": {
+        "lastModified": 1681028828,
+        "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=",
+        "owner": "nix-systems",
+        "repo": "default",
+        "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e",
+        "type": "github"
+      },
+      "original": {
+        "owner": "nix-systems",
+        "repo": "default",
+        "type": "github"
+      }
+    }
+  },
+  "root": "root",
+  "version": 7
+}

flake.nix

@@ -0,0 +1,15 @@
+{
+  description = "Flake for compiling my bachelor's thesis";
+
+  inputs.nixpkgs.url = "github:NixOS/nixpkgs/nixos-23.05";
+  inputs.flake-utils.url = "github:numtide/flake-utils";
+
+  outputs = { self, nixpkgs, flake-utils }:
+    flake-utils.lib.eachDefaultSystem
+      (system:
+        let pkgs = nixpkgs.legacyPackages.${system}; in
+        {
+          devShells.default = import ./shell.nix { inherit pkgs; };
+        }
+      );
+}

index.lagda.md

@@ -38,7 +38,8 @@ open import Category.Construction.UniformIterationAlgebras
 Existence of free uniform-iteration algebras yields a monad that is of interest to us, we call it **K** and want to show some of it's properties (i.e. that it is strong and an equational lifting monad):
 
 ```agda
-open import Monad.Instance.K -- TODO move to Monad.Construction.K
+open import Monad.Instance.K
+open import Monad.Instance.K.Strong
 ```
 
 Later we will also show that free uniform-iteration algebras coincide with free elgot algebras

shell.nix

@@ -0,0 +1,23 @@
+{ pkgs ? import <nixpkgs> { } }:
+with pkgs;
+mkShell {
+  buildInputs = [
+    (agda.withPackages [ 
+      agdaPackages.standard-library 
+      (agdaPackages.agda-categories.overrideAttrs (oldAttrs : {
+        version = "0.1.8";
+        src = fetchFromGitHub {
+          repo = "agda-categories";
+          owner = "Reijix";
+          rev = "102a0c46c7c9be4e47085b745abd1c486b86f0e7";
+          hash = "sha256-1LzbtsqEPSfAyOztqNOG/pT6g1zsyc6lY2NwQqBZQZ8=";
+        };
+      }))
+    ])
+  ];
+
+  shellHook = ''
+    # ...
+  '';
+}
+

src/Monad/Instance/Delay/Lemmas.lagda.md

@@ -1,5 +1,6 @@
 <!--
 ```agda
+{-# OPTIONS --allow-unsolved-metas #-}
 open import Level
 open import Category.Instance.AmbientCategory
 open import Categories.Functor

src/Monad/Instance/K.lagda.md

@@ -1,58 +1,46 @@
 <!--
 ```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 Categories.Monad.Relative renaming (Monad to RMonad)
-open import Categories.Monad.Construction.Kleisli
+open import Categories.FreeObjects.Free using (FreeObject; FO⇒Functor; FO⇒LAdj)
+open import Categories.Functor.Core using (Functor)
+open import Categories.Adjoint using (_⊣_)
+open import Categories.Adjoint.Properties using (adjoint⇒monad)
+open import Categories.Monad using (Monad)
+open import Categories.Monad.Relative using () renaming (Monad to RMonad)
 open import Category.Instance.AmbientCategory using (Ambient)
-open import Categories.NaturalTransformation
-open import Categories.Object.Terminal
--- open import Data.Product using (_,_; Σ; Σ-syntax)
+open import Categories.Monad.Construction.Kleisli
 ```
 -->
 
-## 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
+# The monad K
 
 ```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 import Category.Construction.UniformIterationAlgebras ambient using (Uniform-Iteration-Algebras)
+  open import Algebra.UniformIterationAlgebra ambient using (Uniform-Iteration-Algebra)
   open import Algebra.Properties ambient using (FreeUniformIterationAlgebra; uniformForgetfulF; IsStableFreeUniformIterationAlgebra)
 
   open Equiv
   open MR C
   open M C
   open HomReasoning
-
 ```
 
-### *Lemma 16*: definition of monad ***K***
+## Definition
+
+The monad is defined by existence of free uniform-iteration algebras. 
+Since free objects yield and adjunctions, this yields a monad.
 
 ```agda
   record MonadK : Set (suc o ⊔ suc ℓ ⊔ suc e) where
     field
       freealgebras : ∀ X → FreeUniformIterationAlgebra X
+      stable : ∀ X → IsStableFreeUniformIterationAlgebra (freealgebras X)
+
+    -- helper for accessing ui-algebras
+    algebras : ∀ (X : Obj) → Uniform-Iteration-Algebra
+    algebras X = FreeObject.FX (freealgebras X)
 
     freeF : Functor C Uniform-Iteration-Algebras
     freeF = FO⇒Functor uniformForgetfulF freealgebras
@@ -60,223 +48,13 @@ module Monad.Instance.K {o ℓ e} (ambient : Ambient o ℓ e) where
     adjoint : freeF ⊣ uniformForgetfulF
     adjoint = FO⇒LAdj uniformForgetfulF freealgebras
 
-    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
-      freealgebras : ∀ X → FreeUniformIterationAlgebra X
-      stable : ∀ X → IsStableFreeUniformIterationAlgebra (freealgebras X)
-    
-    algebras : ∀ (X : Obj) → Uniform-Iteration-Algebra
-    algebras X = FreeObject.FX (freealgebras X)
-
-    K : Monad C
-    K = MonadK.K (record { freealgebras = freealgebras })
-
-    open Monad K using (F; μ) renaming (identityʳ to m-identityʳ)
-    module kleisli = RMonad (Monad⇒Kleisli C K)
-    open kleisli using (extend)
-    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ˡ = identityˡ'
-        ; η-comm = λ {A} {B} → τ-η (A , B)
-        ; μ-η-comm = μ-η-comm'
-        ; strength-assoc = strength-assoc'
-        }
-      }
-      where
-        open import Agda.Builtin.Sigma
-        open IsStableFreeUniformIterationAlgebra using (♯-law; ♯-preserving; ♯-unique)
-        open Uniform-Iteration-Algebra using (#-Uniformity; #-Fixpoint; #-resp-≈)
-        η = λ Z → FreeObject.η (freealgebras Z)
-        _♯ = λ {A X Y} f → IsStableFreeUniformIterationAlgebra.[_,_]♯ {Y = X} (stable X) {X = A} (algebras Y) f
-        _# = λ {A} {X} f → Uniform-Iteration-Algebra._# (algebras A) {X = X} f
-
-        module _ (P : Category.Obj (CProduct C C)) where
-          private
-            X = fst P
-            Y = snd P
-          τ : X × K₀ Y ⇒ K₀ (X × Y)
-          τ = η (X × Y) ♯
-
-          τ-η : τ ∘ (idC ⁂ η Y) ≈ η (X × Y)
-          τ-η = sym (♯-law (stable Y) (η (X × Y)))
-
-        τ-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 K f)) ⟩∘⟨refl ⟩ 
-          extend (η Y ∘ f) ∘ η X ≈⟨ kleisli.identityʳ ⟩ 
-          η Y ∘ f ∎
-
-        μ-η-comm' : ∀ {A B} → μ.η _ ∘ K₁ (τ _) ∘ τ (A , K₀ B) ≈ τ _ ∘ (idC ⁂ μ.η _)
-        μ-η-comm' {A} {B} = begin 
-          μ.η _ ∘ K₁ (τ _) ∘ τ _ ≈⟨ ♯-unique (stable (K₀ B)) (τ (A , B)) (μ.η _ ∘ K₁ (τ _) ∘ τ _) comm₁ comm₂ ⟩ 
-          (τ _ ♯) ≈⟨ sym (♯-unique (stable (K₀ B)) (τ (A , B)) (τ _ ∘ (idC ⁂ μ.η _)) (sym (cancelʳ (⁂∘⁂ ○ ⁂-cong₂ identity² m-identityʳ ○ ⟨⟩-unique id-comm id-comm))) comm₃) ⟩ 
-          τ _ ∘ (idC ⁂ μ.η _) ∎
-          where
-            comm₁ : τ (A , B) ≈ (μ.η _ ∘ K₁ (τ _) ∘ τ _) ∘ (idC ⁂ η _)
-            comm₁ = sym (begin 
-              (μ.η _ ∘ K₁ (τ _) ∘ τ _) ∘ (idC ⁂ η _) ≈⟨ pullʳ (pullʳ (τ-η _)) ⟩ 
-              μ.η _ ∘ K₁ (τ _) ∘ η _ ≈⟨ refl⟩∘⟨ (K₁η (τ (A , B))) ⟩ 
-              μ.η _ ∘ η _ ∘ τ _ ≈⟨ cancelˡ m-identityʳ ⟩ 
-              τ _ ∎)
-            comm₂ : ∀ {Z : Obj} (h : Z ⇒ K₀ (K₀ B) + Z) → (μ.η _ ∘ K₁ (τ _) ∘ τ _) ∘ (idC ⁂ h #) ≈ ((μ.η _ ∘ K₁ (τ (A , B)) ∘ τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #
-            comm₂ {Z} h = begin 
-              (μ.η _ ∘ K₁ (τ _) ∘ τ _) ∘ (idC ⁂ h #) ≈⟨ pullʳ (pullʳ (τ-comm h)) ⟩ 
-              μ.η _ ∘ K₁ (τ _) ∘ (((τ (A , K₀ B) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #) ≈⟨ refl⟩∘⟨ (Uniform-Iteration-Algebra-Morphism.preserves (((freealgebras _) FreeObject.*) (η _ ∘ τ _))) ⟩ 
-              μ.η _ ∘ ((K₁ (τ _) +₁ idC) ∘ (τ (A , K₀ B) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈⟨ Uniform-Iteration-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)) # ∎
-            comm₃ : ∀ {Z : Obj} (h : Z ⇒ K₀ (K₀ B) + Z) → (τ _ ∘ (idC ⁂ μ.η _)) ∘ (idC ⁂ h #) ≈ ((τ _ ∘ (idC ⁂ μ.η _) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #
-            comm₃ {Z} h = begin 
-              (τ _ ∘ (idC ⁂ μ.η _)) ∘ (idC ⁂ h #) ≈⟨ pullʳ ⁂∘⁂ ⟩ 
-              τ _ ∘ (idC ∘ idC ⁂ μ.η _ ∘ h #) ≈⟨ refl⟩∘⟨ (⁂-cong₂ identity² (Uniform-Iteration-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₁ 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)) # ∎
-
-        module assoc {A} {B} {C} = _≅_ (×-assoc {A} {B} {C})
-
-        strength-assoc' : ∀ {X Y Z} → K₁ assoc.to ∘ τ (X × Y , Z) ≈ τ (X , Y × Z) ∘ (idC ⁂ τ (Y , Z)) ∘ assoc.to
-        strength-assoc' {X} {Y} {Z} = begin
-          K₁ assoc.to ∘ τ _ ≈⟨ ♯-unique (stable _) (η (X × Y × Z) ∘ assoc.to) (K₁ assoc.to ∘ τ _) (sym (pullʳ (τ-η _) ○ K₁η _)) comm₁ ⟩ 
-          ((η (X × Y × Z) ∘ assoc.to) ♯) ≈⟨ sym (♯-unique (stable _) (η (X × Y × Z) ∘ assoc.to) (τ _ ∘ (idC ⁂ τ _) ∘ assoc.to) comm₂ comm₃) ⟩
-          τ _ ∘ (idC ⁂ τ _) ∘ assoc.to ∎
-          where
-            comm₁ : ∀ {A : Obj} (h : A ⇒ K₀ Z + A) → (K₁ assoc.to ∘ τ _) ∘ (idC ⁂ h #) ≈ ((K₁ assoc.to ∘ τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #
-            comm₁ {A} h = begin 
-              (K₁ assoc.to ∘ τ _) ∘ (idC ⁂ h #) ≈⟨ pullʳ (τ-comm h) ⟩ 
-              K₁ assoc.to ∘ ((τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# ≈⟨ Uniform-Iteration-Algebra-Morphism.preserves (((freealgebras _) FreeObject.*) _) ⟩ 
-              ((K₁ assoc.to +₁ idC) ∘ (τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# ≈⟨ #-resp-≈ (algebras _) (pullˡ (+₁∘+₁ ○ +₁-cong₂ refl identity²)) ⟩ 
-              ((K₁ assoc.to ∘ τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ∎
-            comm₂ : η (X × Y × Z) ∘ assoc.to ≈ (τ _ ∘ (idC ⁂ τ _) ∘ assoc.to) ∘ (idC ⁂ η _)
-            comm₂ = sym (begin 
-              (τ _ ∘ (idC ⁂ τ _) ∘ assoc.to) ∘ (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.to ∎)
-            comm₃ : ∀ {A : Obj} (h : A ⇒ K₀ Z + A) → (τ _ ∘ (idC ⁂ τ _) ∘ assoc.to) ∘ (idC ⁂ h #) ≈ ((τ _ ∘ (idC ⁂ τ _) ∘ assoc.to +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #
-            comm₃ {A} h = begin 
-              (τ _ ∘ (idC ⁂ τ _) ∘ assoc.to) ∘ (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.to ≈⟨ pullˡ (τ-comm _) ⟩ 
-              ((τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ (τ (Y , Z) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))) # ∘ assoc.to ≈⟨ sym (#-Uniformity (algebras _) (begin 
-                (idC +₁ assoc.to) ∘ (τ _ ∘ (idC ⁂ τ (Y , Z)) ∘ assoc.to +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ≈⟨ pullˡ +₁∘+₁ ⟩ 
-                (idC ∘ τ _ ∘ (idC ⁂ τ (Y , Z)) ∘ assoc.to +₁ assoc.to ∘ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ≈⟨ (+₁-cong₂ identityˡ id-comm) ⟩∘⟨refl ⟩ 
-                (τ _ ∘ (idC ⁂ τ (Y , Z)) ∘ assoc.to +₁ idC ∘ assoc.to) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ≈˘⟨ (+₁∘+₁ ○ +₁-cong₂ assoc refl) ⟩∘⟨refl ⟩ 
-                ((τ _ ∘ (idC ⁂ τ (Y , Z)) +₁ idC) ∘ (assoc.to +₁ assoc.to)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ≈⟨ pullʳ (pullˡ (sym distributeˡ⁻¹-assoc)) ⟩ 
-                (τ _ ∘ (idC ⁂ τ (Y , Z)) +₁ idC) ∘ (distributeˡ⁻¹ ∘ (idC ⁂ distributeˡ⁻¹) ∘ assoc.to) ∘ (idC ⁂ h) ≈⟨ refl⟩∘⟨ assoc²' ⟩ 
-                (τ _ ∘ (idC ⁂ τ _) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ distributeˡ⁻¹) ∘ assoc.to ∘ (idC ⁂ h) ≈˘⟨ (+₁-cong₂ refl (elimʳ (⟨⟩-unique id-comm id-comm))) ⟩∘⟨refl ⟩ 
-                (τ _ ∘ (idC ⁂ τ _) +₁ idC ∘ (idC ⁂ idC)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ distributeˡ⁻¹) ∘ assoc.to ∘ (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.to ∘ (idC ⁂ h) ≈⟨ refl⟩∘⟨ ((distribute₁ idC (τ (Y , Z)) idC) ⟩∘⟨refl) ⟩∘⟨refl ⟩ 
-                (τ _ +₁ idC) ∘ ((distributeˡ⁻¹ ∘ (idC ⁂ (τ (Y , Z) +₁ idC))) ∘ (idC ⁂ distributeˡ⁻¹)) ∘ assoc.to ∘ (idC ⁂ h) ≈⟨ refl⟩∘⟨ (assoc ○ assoc ○ refl⟩∘⟨ sym-assoc) ⟩
-                (τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ ((idC ⁂ (τ (Y , Z) +₁ idC)) ∘ (idC ⁂ distributeˡ⁻¹)) ∘ assoc.to ∘ (idC ⁂ h) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (⁂∘⁂ ○ ⁂-cong₂ identity² refl) ⟩∘⟨refl ⟩ 
-                (τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ (τ (Y , Z) +₁ idC) ∘ distributeˡ⁻¹) ∘ assoc.to ∘ (idC ⁂ h) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ ⁂-cong₂ (sym (⟨⟩-unique id-comm id-comm)) refl ⟩ 
-                (τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ (τ (Y , Z) +₁ idC) ∘ distributeˡ⁻¹) ∘ assoc.to ∘ ((idC ⁂ idC) ⁂ h) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ assocˡ∘⁂ ⟩ 
-                (τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ (τ (Y , Z) +₁ idC) ∘ distributeˡ⁻¹) ∘ (idC ⁂ (idC ⁂ h)) ∘ assoc.to ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ assoc ⟩
-                (τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ ((idC ⁂ (τ (Y , Z) +₁ idC) ∘ distributeˡ⁻¹) ∘ (idC ⁂ (idC ⁂ h))) ∘ assoc.to ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⁂∘⁂ ⟩∘⟨refl ⟩ 
-                (τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ∘ idC ⁂ ((τ (Y , Z) +₁ idC) ∘ distributeˡ⁻¹) ∘ (idC ⁂ h)) ∘ assoc.to ≈⟨ refl⟩∘⟨ (refl⟩∘⟨ ((⁂-cong₂ identity² assoc) ⟩∘⟨refl) ○ sym-assoc) ○ sym-assoc ⟩
-                ((τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ (τ (Y , Z) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))) ∘ assoc.to ∎)) ⟩
-              ((τ _ ∘ (idC ⁂ τ _) ∘ assoc.to +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ 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 ⁂ K₁ g) ≈⟨ ♯-unique (stable V) (η (W × X) ∘ (f ⁂ g)) (τ _ ∘ (f ⁂ K₁ g)) comm₁ comm₂ ⟩ 
-          (η _ ∘ (f ⁂ g)) ♯ ≈⟨ sym (♯-unique (stable V) (η (W × X) ∘ (f ⁂ g)) (K₁ (f ⁂ g) ∘ τ _) comm₃ comm₄) ⟩
-          K₁ (f ⁂ g) ∘ τ _ ∎
-          where
-            comm₁ : η (W × X) ∘ (f ⁂ g) ≈ (τ (W , X) ∘ (f ⁂ K₁ g)) ∘ (idC ⁂ η V)
-            comm₁ = 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) ∎)
-            comm₃ : η (W × X) ∘ (f ⁂ g) ≈ (K₁ (f ⁂ g) ∘ τ (U , V)) ∘ (idC ⁂ η V)
-            comm₃ = sym (begin
-              (K₁ (f ⁂ g) ∘ τ (U , V)) ∘ (idC ⁂ η V) ≈⟨ pullʳ (τ-η (U , V)) ⟩ 
-              K₁ (f ⁂ g) ∘ η (U × V) ≈⟨ K₁η (f ⁂ g) ⟩ 
-              η (W × X) ∘ (f ⁂ g) ∎)
-            comm₂ : ∀ {Z : Obj} (h : Z ⇒ K₀ V + Z) → (τ (W , X) ∘ (f ⁂ K₁ g)) ∘ (idC ⁂ h #) ≈ ((τ (W , X) ∘ (f ⁂ K₁ g) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))#
-            comm₂ {Z} h = begin 
-              (τ (W , X) ∘ (f ⁂ K₁ g)) ∘ (idC ⁂ h #) ≈⟨ pullʳ ⁂∘⁂ ⟩ 
-              τ (W , X) ∘ (f ∘ idC ⁂ K₁ g ∘ (h #)) ≈⟨ refl⟩∘⟨ (⁂-cong₂ id-comm ((Uniform-Iteration-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 _) (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₁ 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) ∎)) ⟩ 
-              ((τ (W , X) ∘ (f ⁂ K₁ g) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# ∎ 
-            comm₄ : ∀ {Z : Obj} (h : Z ⇒ K₀ V + Z) → (K₁ (f ⁂ g) ∘ τ (U , V)) ∘ (idC ⁂ h #) ≈ ((K₁ (f ⁂ g) ∘ τ (U , V) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #
-            comm₄ {Z} h = begin 
-              (K₁ (f ⁂ g) ∘ τ (U , V)) ∘ (idC ⁂ (h #)) ≈⟨ pullʳ (τ-comm h) ⟩ 
-              K₁ (f ⁂ g) ∘ ((τ (U , V) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈⟨ Uniform-Iteration-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)) # ∎
-
-        identityˡ' : ∀ {X : Obj} → K₁ π₂ ∘ τ _ ≈ π₂
-        identityˡ' {X} = begin 
-          K₁ π₂ ∘ τ _ ≈⟨ ♯-unique (stable X) (η X ∘ π₂) (K₁ π₂ ∘ τ (Terminal.⊤ terminal , X)) comm₁ comm₂ ⟩
-          (η X ∘ π₂) ♯ ≈⟨ sym (♯-unique (stable X) (η X ∘ π₂) π₂ (sym π₂∘⁂) comm₃) ⟩
-          π₂ ∎
-          where
-            comm₁ : η X ∘ π₂ ≈ (K₁ π₂ ∘ τ (Terminal.⊤ terminal , X)) ∘ (idC ⁂ η X)
-            comm₁ = sym (begin 
-              (K₁ π₂ ∘ τ (Terminal.⊤ terminal , X)) ∘ (idC ⁂ η X) ≈⟨ pullʳ (τ-η (Terminal.⊤ terminal , X)) ⟩ 
-              K₁ π₂ ∘ η (Terminal.⊤ terminal × X) ≈⟨ (sym (F₁⇒extend K π₂)) ⟩∘⟨refl ⟩
-              extend (η _ ∘ π₂) ∘ η _ ≈⟨ kleisli.identityʳ ⟩
-              η X ∘ π₂ ∎)
-            comm₂ : ∀ {Z : Obj} (h : Z ⇒ K₀ X + Z) → (K₁ π₂ ∘ τ (Terminal.⊤ terminal , X)) ∘ (idC ⁂ h # ) ≈ ((K₁ π₂ ∘ τ (Terminal.⊤ terminal , X) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))#
-            comm₂ {Z} h = begin
-              (K₁ π₂ ∘ τ _) ∘ (idC ⁂ h #) ≈⟨ pullʳ (♯-preserving (stable X) (η _) h) ⟩ 
-              K₁ π₂ ∘ ((τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈⟨ Uniform-Iteration-Algebra-Morphism.preserves ((freealgebras (Terminal.⊤ terminal × X) FreeObject.*) (η X ∘ π₂)) ⟩
-              ((K₁ π₂ +₁ idC) ∘ (τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈⟨ #-resp-≈ (algebras X) (pullˡ (+₁∘+₁ ○ +₁-cong₂ refl identity²)) ⟩
-              ((K₁ π₂ ∘ τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# ∎
-            comm₃ : ∀ {Z : Obj} (h : Z ⇒ K₀ X + Z) → π₂ ∘ (idC ⁂ h #) ≈ ((π₂ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #
-            comm₃ {Z} h = begin 
-              π₂ ∘ (idC ⁂ h #) ≈⟨ π₂∘⁂ ⟩ 
-              h # ∘ π₂ ≈⟨ sym (#-Uniformity (algebras X) (begin 
-                (idC +₁ π₂) ∘ (π₂ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ≈⟨ pullˡ +₁∘+₁ ⟩ 
-                (idC ∘ π₂ +₁ π₂ ∘ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ≈⟨ (+₁-cong₂ identityˡ identityʳ) ⟩∘⟨refl ⟩ 
-                (π₂ +₁ π₂) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ≈⟨ pullˡ dstr-law₅ ⟩ 
-                π₂ ∘ (idC ⁂ h) ≈⟨ project₂ ⟩ 
-                h ∘ π₂ ∎)) ⟩ 
-              ((π₂ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ∎
+    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
 ```

src/Monad/Instance/K/Commutative.lagda.md

@@ -0,0 +1,84 @@
+<!--
+```agda
+open import Level
+open import Category.Instance.AmbientCategory
+open import Monad.Commutative
+open import Categories.Monad.Strong
+open import Data.Product using (_,_) renaming (_×_ to _×f_)
+open import Categories.FreeObjects.Free
+import Monad.Instance.K as MIK
+```
+-->
+
+```agda
+module Monad.Instance.K.Commutative {o ℓ e} (ambient : Ambient o ℓ e) (MK : MIK.MonadK ambient) where
+  open Ambient ambient
+  open MIK ambient
+  open MonadK MK
+  open import Monad.Instance.K.Strong ambient MK
+  open import Category.Construction.UniformIterationAlgebras ambient
+  open import Algebra.UniformIterationAlgebra ambient
+  open import Algebra.Properties ambient using (FreeUniformIterationAlgebra; uniformForgetfulF; IsStableFreeUniformIterationAlgebra)
+
+  open Equiv
+  open HomReasoning
+  open MR C
+  -- open M C
+```
+
+# K is a commutative monad
+The proof is analogous to the ones for strength, this is the relevant diagram is:
+
+<!-- https://q.uiver.app/#q=WzAsNyxbMCwxLCJLWCBcXHRpbWVzIEtZIl0sWzEsMCwiSyhLWCBcXHRpbWVzIFkpIl0sWzIsMCwiSyhLKFggXFx0aW1lcyBZKSkiXSxbMywxLCJLKFggXFx0aW1lcyBZKSJdLFsxLDIsIksoWCBcXHRpbWVzIEtZKSJdLFsyLDIsIksoSyhYIFxcdGltZXMgWSkpIl0sWzAsNCwiS1ggXFx0aW1lcyBZIl0sWzAsMSwiXFx0YXUiXSxbMSwyLCJcXGhhdHtcXHRhdX1eKiJdLFsyLDMsIlxcbXUiXSxbMCw0LCJcXGhhdHtcXHRhdX0iLDJdLFs0LDUsIlxcdGF1XioiLDJdLFs1LDMsIlxcbXUiLDJdLFs2LDAsImlkIFxcdGltZXMgXFxldGEiXSxbNiwzLCJcXGhhdHtcXHRhdX0iLDAseyJjdXJ2ZSI6NX1dLFswLDMsIlxcaGF0e1xcdGF1fV5cXCMiXV0= -->
+<iframe class="quiver-embed" src="https://q.uiver.app/#q=WzAsNyxbMCwxLCJLWCBcXHRpbWVzIEtZIl0sWzEsMCwiSyhLWCBcXHRpbWVzIFkpIl0sWzIsMCwiSyhLKFggXFx0aW1lcyBZKSkiXSxbMywxLCJLKFggXFx0aW1lcyBZKSJdLFsxLDIsIksoWCBcXHRpbWVzIEtZKSJdLFsyLDIsIksoSyhYIFxcdGltZXMgWSkpIl0sWzAsNCwiS1ggXFx0aW1lcyBZIl0sWzAsMSwiXFx0YXUiXSxbMSwyLCJcXGhhdHtcXHRhdX1eKiJdLFsyLDMsIlxcbXUiXSxbMCw0LCJcXGhhdHtcXHRhdX0iLDJdLFs0LDUsIlxcdGF1XioiLDJdLFs1LDMsIlxcbXUiLDJdLFs2LDAsImlkIFxcdGltZXMgXFxldGEiXSxbNiwzLCJcXGhhdHtcXHRhdX0iLDAseyJjdXJ2ZSI6NX1dLFswLDMsIlxcaGF0e1xcdGF1fV5cXCMiXV0=&embed" width="974" height="688" style="border-radius: 8px; border: none;"></iframe>
+
+```agda
+  KCommutative : CommutativeMonad {C = C} {V = monoidal} symmetric KStrong
+  KCommutative = record { commutes = commutes' }
+    where
+      open monadK using (μ)
+      open StrongMonad KStrong
+      open IsStableFreeUniformIterationAlgebra using (♯-law; ♯-preserving; ♯-unique)
+      open Uniform-Iteration-Algebra using (#-Uniformity; #-Fixpoint; #-resp-≈)
+      
+      -- some helper definitions to make our life easier
+      η = λ Z → FreeObject.η (freealgebras Z)
+      _♯ = λ {A X Y} f → IsStableFreeUniformIterationAlgebra.[_,_]♯ {Y = X} (stable X) {X = A} (algebras Y) f
+      _# = λ {A} {X} f → Uniform-Iteration-Algebra._# (algebras A) {X = X} f
+
+      σ : ∀ ((X , Y) : Obj ×f Obj) → K.₀ X × Y ⇒ K.₀ (X × Y)
+      σ _ = K.₁ swap ∘ (τ _) ∘ swap
+      commutes' : ∀ {X Y : Obj} → μ.η _ ∘ K.₁ (σ _) ∘ τ (K.₀ X , Y) ≈ μ.η _ ∘ K.₁ (τ _) ∘ σ _
+      commutes' {X} {Y} = begin 
+        μ.η _ ∘ K.₁ (σ _) ∘ τ _ ≈⟨ ♯-unique (stable _) (σ _) (μ.η (X × Y) ∘ K.₁ (σ _) ∘ τ _) comm₁ comm₂ ⟩ 
+        (σ _) ♯ ≈⟨ sym (♯-unique (stable _) (σ _) (μ.η _ ∘ K.₁ (τ _) ∘ σ _) comm₃ {!   !}) ⟩ 
+        μ.η _ ∘ K.₁ (τ _) ∘ σ _ ∎
+        where
+          comm₁ : σ _ ≈ (μ.η _ ∘ K.₁ (σ _) ∘ τ _) ∘ (idC ⁂ η _)
+          comm₁ = sym (begin 
+            (μ.η _ ∘ K.₁ (σ _) ∘ τ _) ∘ (idC ⁂ η _) ≈⟨ pullʳ (pullʳ (τ-η _)) ⟩ 
+            μ.η _ ∘ K.₁ (σ _) ∘ η _ ≈⟨ refl⟩∘⟨ (K₁η _) ⟩
+            μ.η _ ∘ η _ ∘ σ _ ≈⟨ cancelˡ monadK.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ʳ (pullʳ (♯-preserving (stable _) (η _) h)) ⟩ 
+            μ.η _ ∘ K.₁ (σ _) ∘ ((τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈⟨ refl⟩∘⟨ (Uniform-Iteration-Algebra-Morphism.preserves ((freealgebras _ FreeObject.*) (η _ ∘ σ _))) ⟩
+            μ.η _ ∘ ((K.₁ (σ _) +₁ idC) ∘ (τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈⟨ Uniform-Iteration-Algebra-Morphism.preserves (((freealgebras _) FreeObject.*) idC) ⟩
+            ((μ.η _ +₁ idC) ∘ (K.₁ (σ _) +₁ idC) ∘ (τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈⟨ #-resp-≈ (algebras _) (pullˡ +₁∘+₁) ⟩
+            ((μ.η _ ∘ K.₁ (σ _) +₁ idC ∘ idC) ∘ (τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈⟨ #-resp-≈ (algebras _) (pullˡ +₁∘+₁) ⟩
+            (((μ.η _ ∘ K.₁ (σ _)) ∘ τ _ +₁ (idC ∘ idC) ∘ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈⟨ #-resp-≈ (algebras _) ((+₁-cong₂ assoc (elimˡ identity²)) ⟩∘⟨refl) ⟩
+            ((μ.η _ ∘ K.₁ (σ _) ∘ τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# ∎
+          comm₃ : σ _ ≈ (μ.η _ ∘ K.₁ (τ _) ∘ σ _) ∘ (idC ⁂ η _)
+          comm₃ = sym (begin 
+            -- idea use swap epi and K.₁ swap mono:
+            {-
+            K.₁ swap ∘ (μ.η _ ∘ K.₁ (K.₁ swap ∘ τ _) ∘ σ _) ∘ (idC ⁂ η _) ∘ swap
+            ≈ (μ.η _ ∘ K.₁ (σ _) ∘ (τ _)) ∘ (η _ ⁂ idC)
+            -}
+            (μ.η _ ∘ K.₁ (τ _) ∘ σ _) ∘ (idC ⁂ η _) ≈⟨ {!   !} ⟩ 
+            {!   !} ≈⟨ {!   !} ⟩ 
+            {!   !} ≈⟨ {!   !} ⟩ 
+            {!   !} ≈⟨ {!   !} ⟩ 
+            σ _ ∎)
+```

src/Monad/Instance/K/Strong.lagda.md

@@ -0,0 +1,268 @@
+<!--
+```agda
+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
+open import Categories.Monad.Strong
+open import Categories.Monad.Relative renaming (Monad to RMonad)
+open import Category.Instance.AmbientCategory using (Ambient)
+open import Categories.NaturalTransformation
+open import Categories.Object.Terminal
+
+import Monad.Instance.K as MIK
+```
+-->
+
+```agda
+module Monad.Instance.K.Strong {o ℓ e} (ambient : Ambient o ℓ e) (MK : MIK.MonadK ambient) where
+  open Ambient ambient
+  open import Category.Construction.UniformIterationAlgebras ambient
+  open import Algebra.UniformIterationAlgebra ambient
+  open import Algebra.Properties ambient using (FreeUniformIterationAlgebra; uniformForgetfulF; IsStableFreeUniformIterationAlgebra)
+
+  open MIK ambient
+  open MonadK MK
+  open Equiv
+  open MR C
+  open M C
+  open HomReasoning
+```
+
+
+# The monad K is strong
+
+K is a strong monad with the strength defined as `η ♯`, where ♯ is the operator we get from stability.
+Verifying the axioms of strength is straightforward once you know the procedure, since the proofs are all very similar.
+
+For example the proof of `identityˡ` i.e. `K₁ π₂ ∘ τ ≈ π₂` goes as follows:
+
+1. find a morphism `f` such that `K₁ π₂ ∘ τ ≈ f ♯ ≈ π₂`
+2. show that `K₁ π₂ ∘ τ` is iteration preserving and satisfies the stabiltiy law
+3. show that `π₂` is iteration preserving and satisfies the stabiltiy law
+
+=> by uniqueness of `f ♯` we are done
+
+The following diagram demonstrates this:
+
+<!-- https://q.uiver.app/#q=WzAsNCxbMCwwLCJYXFx0aW1lcyBLWSJdLFsxLDEsIksoWFxcdGltZXMgWSkiXSxbMCwyLCJYXFx0aW1lcyBZIl0sWzIsMCwiS1kiXSxbMCwxLCJcXGV0YV57XFwjfSJdLFsyLDAsImlkXFx0aW1lc1xcZXRhIl0sWzIsMSwiXFxldGEiLDJdLFsxLDMsIktcXHBpXzIiXSxbMCwzLCJcXHBpXzI9KFxcZXRhXFxjaXJjXFxwaV8yKV57XFwjfSJdLFsyLDMsIlxcZXRhXFxjaXJjXFxwaV8yIiwyLHsiY3VydmUiOjR9XV0= -->
+<iframe class="quiver-embed" src="https://q.uiver.app/#q=WzAsNCxbMCwwLCJYXFx0aW1lcyBLWSJdLFsxLDEsIksoWFxcdGltZXMgWSkiXSxbMCwyLCJYXFx0aW1lcyBZIl0sWzIsMCwiS1kiXSxbMCwxLCJcXGV0YV57XFwjfSJdLFsyLDAsImlkXFx0aW1lc1xcZXRhIl0sWzIsMSwiXFxldGEiLDJdLFsxLDMsIktcXHBpXzIiXSxbMCwzLCJcXHBpXzI9KFxcZXRhXFxjaXJjXFxwaV8yKV57XFwjfSJdLFsyLDMsIlxcZXRhXFxjaXJjXFxwaV8yIiwyLHsiY3VydmUiOjR9XV0=&embed" width="571" height="432" style="border-radius: 8px; border: none;"></iframe>
+
+```agda
+  -- we use properties of the kleisli representation as well as the 'normal' monad representation
+  open kleisliK using (extend)
+  open monadK using (μ)
+
+  -- defining τ
+  private
+    -- some helper definitions to make our life easier
+    η = λ Z → FreeObject.η (freealgebras Z)
+    _♯ = λ {A X Y} f → IsStableFreeUniformIterationAlgebra.[_,_]♯ {Y = X} (stable X) {X = A} (algebras Y) f
+    _# = λ {A} {X} f → Uniform-Iteration-Algebra._# (algebras A) {X = X} f
+
+  open IsStableFreeUniformIterationAlgebra using (♯-law; ♯-preserving; ♯-unique)
+  open Uniform-Iteration-Algebra using (#-Uniformity; #-Fixpoint; #-resp-≈)
+
+  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)))
+
+  τ-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                ∎
+
+  KStrength : Strength monoidal monadK
+  KStrength = record
+    { strengthen = ntHelper (record { η = τ ; commute = commute' })
+    ; identityˡ = identityˡ'
+    ; η-comm = λ {A} {B} → τ-η (A , B)
+    ; μ-η-comm = μ-η-comm'
+    ; strength-assoc = strength-assoc'
+    }
+    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) = begin 
+        τ _ ∘ (f ⁂ K.₁ g) ≈⟨ ♯-unique (stable V) (η (W × X) ∘ (f ⁂ g)) (τ _ ∘ (f ⁂ K.₁ g)) comm₁ comm₂ ⟩ 
+        (η _ ∘ (f ⁂ g)) ♯ ≈⟨ sym (♯-unique (stable V) (η (W × X) ∘ (f ⁂ g)) (K.₁ (f ⁂ g) ∘ τ _) comm₃ comm₄) ⟩
+        K.₁ (f ⁂ g) ∘ τ _ ∎
+        where
+          comm₁ : η (W × X) ∘ (f ⁂ g) ≈ (τ (W , X) ∘ (f ⁂ K.₁ g)) ∘ (idC ⁂ η V)
+          comm₁ = 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)                     ∎)
+          comm₃ : η (W × X) ∘ (f ⁂ g) ≈ (K.₁ (f ⁂ g) ∘ τ (U , V)) ∘ (idC ⁂ η V)
+          comm₃ = sym (begin
+            (K.₁ (f ⁂ g) ∘ τ (U , V)) ∘ (idC ⁂ η V) ≈⟨ pullʳ (τ-η (U , V)) ⟩ 
+            K.₁ (f ⁂ g) ∘ η (U × V)                 ≈⟨ K₁η (f ⁂ g) ⟩ 
+            η (W × X) ∘ (f ⁂ g)                     ∎)
+          comm₂ : ∀ {Z : Obj} (h : Z ⇒ K.₀ V + Z) → (τ (W , X) ∘ (f ⁂ K.₁ g)) ∘ (idC ⁂ h #) ≈ ((τ (W , X) ∘ (f ⁂ K.₁ g) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))#
+          comm₂ {Z} h = begin 
+            (τ (W , X) ∘ (f ⁂ K.₁ g)) ∘ (idC ⁂ h #)                                         ≈⟨ pullʳ ⁂∘⁂ ⟩ 
+            τ (W , X) ∘ (f ∘ idC ⁂ K.₁ g ∘ (h #))                                           ≈⟨ refl⟩∘⟨ (⁂-cong₂ id-comm ((Uniform-Iteration-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₁ 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)   ∎
+          comm₄ : ∀ {Z : Obj} (h : Z ⇒ K.₀ V + Z) → (K.₁ (f ⁂ g) ∘ τ (U , V)) ∘ (idC ⁂ h #) ≈ ((K.₁ (f ⁂ g) ∘ τ (U , V) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #
+          comm₄ {Z} h = begin 
+            (K.₁ (f ⁂ g) ∘ τ (U , V)) ∘ (idC ⁂ (h #))                                 ≈⟨ pullʳ (τ-comm h) ⟩ 
+            K.₁ (f ⁂ g) ∘ ((τ (U , V) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #          ≈⟨ Uniform-Iteration-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)) #          ∎
+
+      identityˡ' : ∀ {X : Obj} → K.₁ π₂ ∘ τ _ ≈ π₂
+      identityˡ' {X} = begin 
+        K.₁ π₂ ∘ τ _ ≈⟨ ♯-unique (stable X) (η X ∘ π₂) (K.₁ π₂ ∘ τ (Terminal.⊤ terminal , X)) comm₁ comm₂ ⟩
+        (η X ∘ π₂) ♯ ≈⟨ sym (♯-unique (stable X) (η X ∘ π₂) π₂ (sym π₂∘⁂) comm₃) ⟩
+        π₂ ∎
+        where
+          comm₁ : η X ∘ π₂ ≈ (K.₁ π₂ ∘ τ (Terminal.⊤ terminal , X)) ∘ (idC ⁂ η X)
+          comm₁ = sym (begin 
+            (K.₁ π₂ ∘ τ (Terminal.⊤ terminal , X)) ∘ (idC ⁂ η X) ≈⟨ pullʳ (τ-η (Terminal.⊤ terminal , X)) ⟩ 
+            K.₁ π₂ ∘ η (Terminal.⊤ terminal × X)                 ≈⟨ (sym (F₁⇒extend monadK π₂)) ⟩∘⟨refl ⟩
+            extend (η _ ∘ π₂) ∘ η _                              ≈⟨ kleisliK.identityʳ ⟩
+            η X ∘ π₂                                             ∎)
+          comm₂ : ∀ {Z : Obj} (h : Z ⇒ K.₀ X + Z) → (K.₁ π₂ ∘ τ (Terminal.⊤ terminal , X)) ∘ (idC ⁂ h # ) ≈ ((K.₁ π₂ ∘ τ (Terminal.⊤ terminal , X) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))#
+          comm₂ {Z} h = begin
+            (K.₁ π₂ ∘ τ _) ∘ (idC ⁂ h #)                                   ≈⟨ pullʳ (♯-preserving (stable X) (η _) h) ⟩ 
+            K.₁ π₂ ∘ ((τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #          ≈⟨ Uniform-Iteration-Algebra-Morphism.preserves ((freealgebras (Terminal.⊤ terminal × X) FreeObject.*) (η X ∘ π₂)) ⟩
+            ((K.₁ π₂ +₁ idC) ∘ (τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈⟨ #-resp-≈ (algebras X) (pullˡ (+₁∘+₁ ○ +₁-cong₂ refl identity²)) ⟩
+            ((K.₁ π₂ ∘ τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))#           ∎
+          comm₃ : ∀ {Z : Obj} (h : Z ⇒ K.₀ X + Z) → π₂ ∘ (idC ⁂ h #) ≈ ((π₂ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #
+          comm₃ {Z} h = begin 
+            π₂ ∘ (idC ⁂ h #)                            ≈⟨ π₂∘⁂ ⟩ 
+            h # ∘ π₂                                    ≈⟨ sym (#-Uniformity (algebras X) 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ˡ dstr-law₅ ⟩ 
+                π₂ ∘ (idC ⁂ h)                                        ≈⟨ project₂ ⟩ 
+                h ∘ π₂                                                ∎
+
+      μ-η-comm' : ∀ {A B} → μ.η _ ∘ K.₁ (τ _) ∘ τ (A , K.₀ B) ≈ τ _ ∘ (idC ⁂ μ.η _)
+      μ-η-comm' {A} {B} = begin 
+        μ.η _ ∘ K.₁ (τ _) ∘ τ _ ≈⟨ ♯-unique (stable (K.₀ B)) (τ (A , B)) (μ.η _ ∘ K.₁ (τ _) ∘ τ _) comm₁ comm₂ ⟩ 
+        (τ _ ♯)                 ≈⟨ sym (♯-unique (stable (K.₀ B)) (τ (A , B)) (τ _ ∘ (idC ⁂ μ.η _)) (sym (cancelʳ (⁂∘⁂ ○ ⁂-cong₂ identity² monadK.identityʳ ○ ⟨⟩-unique id-comm id-comm))) comm₃) ⟩ 
+        τ _ ∘ (idC ⁂ μ.η _)     ∎
+        where
+          comm₁ : τ (A , B) ≈ (μ.η _ ∘ K.₁ (τ _) ∘ τ _) ∘ (idC ⁂ η _)
+          comm₁ = sym (begin 
+            (μ.η _ ∘ K.₁ (τ _) ∘ τ _) ∘ (idC ⁂ η _) ≈⟨ pullʳ (pullʳ (τ-η _)) ⟩ 
+            μ.η _ ∘ K.₁ (τ _) ∘ η _                 ≈⟨ refl⟩∘⟨ (K₁η (τ (A , B))) ⟩ 
+            μ.η _ ∘ η _ ∘ τ _                       ≈⟨ cancelˡ monadK.identityʳ ⟩ 
+            τ _                                     ∎)
+          comm₂ : ∀ {Z : Obj} (h : Z ⇒ K.₀ (K.₀ B) + Z) → (μ.η _ ∘ K.₁ (τ _) ∘ τ _) ∘ (idC ⁂ h #) ≈ ((μ.η _ ∘ K.₁ (τ (A , B)) ∘ τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #
+          comm₂ {Z} h = begin 
+            (μ.η _ ∘ K.₁ (τ _) ∘ τ _) ∘ (idC ⁂ h #)                                                      ≈⟨ pullʳ (pullʳ (τ-comm h)) ⟩ 
+            μ.η _ ∘ K.₁ (τ _) ∘ (((τ (A , K.₀ B) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #)                 ≈⟨ refl⟩∘⟨ (Uniform-Iteration-Algebra-Morphism.preserves (((freealgebras _) FreeObject.*) (η _ ∘ τ _))) ⟩ 
+            μ.η _ ∘ ((K.₁ (τ _) +₁ idC) ∘ (τ (A , K.₀ B) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #          ≈⟨ Uniform-Iteration-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)) #                       ∎
+          comm₃ : ∀ {Z : Obj} (h : Z ⇒ K.₀ (K.₀ B) + Z) → (τ _ ∘ (idC ⁂ μ.η _)) ∘ (idC ⁂ h #) ≈ ((τ _ ∘ (idC ⁂ μ.η _) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #
+          comm₃ {Z} h = begin 
+            (τ _ ∘ (idC ⁂ μ.η _)) ∘ (idC ⁂ h #)                                         ≈⟨ pullʳ ⁂∘⁂ ⟩ 
+            τ _ ∘ (idC ∘ idC ⁂ μ.η _ ∘ h #)                                             ≈⟨ refl⟩∘⟨ (⁂-cong₂ identity² (Uniform-Iteration-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₁ 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-assoc' : ∀ {X Y Z} → K.₁ assocˡ ∘ τ (X × Y , Z) ≈ τ (X , Y × Z) ∘ (idC ⁂ τ (Y , Z)) ∘ assocˡ
+      strength-assoc' {X} {Y} {Z} = begin
+        K.₁ assocˡ ∘ τ _             ≈⟨ ♯-unique (stable _) (η (X × Y × Z) ∘ assocˡ) (K.₁ assocˡ ∘ τ _) (sym (pullʳ (τ-η _) ○ K₁η _)) comm₁ ⟩ 
+        ((η (X × Y × Z) ∘ assocˡ) ♯) ≈⟨ sym (♯-unique (stable _) (η (X × Y × Z) ∘ assocˡ) (τ _ ∘ (idC ⁂ τ _) ∘ assocˡ) comm₂ comm₃) ⟩
+        τ _ ∘ (idC ⁂ τ _) ∘ assocˡ   ∎
+        where
+          comm₁ : ∀ {A : Obj} (h : A ⇒ K.₀ Z + A) → (K.₁ assocˡ ∘ τ _) ∘ (idC ⁂ h #) ≈ ((K.₁ assocˡ ∘ τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #
+          comm₁ {A} h = begin 
+            (K.₁ assocˡ ∘ τ _) ∘ (idC ⁂ h #)                                  ≈⟨ pullʳ (τ-comm h) ⟩ 
+            K.₁ assocˡ ∘ ((τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))#          ≈⟨ Uniform-Iteration-Algebra-Morphism.preserves (((freealgebras _) FreeObject.*) _) ⟩ 
+            ((K.₁ assocˡ +₁ idC) ∘ (τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# ≈⟨ #-resp-≈ (algebras _) (pullˡ (+₁∘+₁ ○ +₁-cong₂ refl identity²)) ⟩ 
+            ((K.₁ assocˡ ∘ τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #         ∎
+          comm₂ : η (X × Y × Z) ∘ assocˡ ≈ (τ _ ∘ (idC ⁂ τ _) ∘ assocˡ) ∘ (idC ⁂ η _)
+          comm₂ = 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ˡ                                                           ∎)
+          comm₃ : ∀ {A : Obj} (h : A ⇒ K.₀ Z + A) → (τ _ ∘ (idC ⁂ τ _) ∘ assocˡ) ∘ (idC ⁂ h #) ≈ ((τ _ ∘ (idC ⁂ τ _) ∘ assocˡ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #
+          comm₃ {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₁ 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
+    }
+```