minor

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

@@ -289,7 +289,7 @@ and second that `extend f` is the unique morphism satisfying the commutative dia
       ; unit = now
       ; extend = extend'
       ; identityʳ = identityʳ'
-      ; identityˡ = identityˡ'
+      ; identityˡ = extend'-unique now idC (id-comm ○ (sym ([]-unique (identityˡ ○ sym unitlaw) id-comm-sym)) ⟩∘⟨refl)
       ; assoc = assoc'
       ; sym-assoc = sym assoc'
       ; extend-≈ = extend-≈'
@@ -328,20 +328,6 @@ and second that `extend f` is the unique morphism satisfying the commutative dia
           out⁻¹ ∘ out ∘ f                                       ≈⟨ cancelˡ (_≅_.isoˡ out-≅) ⟩
           f                                                     ∎
 
-        identityˡ' : ∀ {X} → extend' now ≈ idC
-        identityˡ' {X} = Terminal.⊤-id (coalgebras X) (record { f = extend' now ; commutes = begin 
-          out ∘ extend' now ≈⟨ pullˡ ((commutes (! (coalgebras X) {A = alg now}))) ⟩ 
-          ((idC +₁ (u (! (coalgebras X) {A = alg now}))) ∘ α (alg now)) ∘ i₁     ≈⟨ pullʳ inject₁ ⟩
-          (idC +₁ (u (! (coalgebras X) {A = alg now}))) 
-          ∘ [ [ i₁ , i₂ ∘ i₂ ] ∘ (out ∘ now) , i₂ ∘ i₁ ] ∘ out                   ≈⟨ refl⟩∘⟨ []-cong₂ ((refl⟩∘⟨ unitlaw) ○ inject₁) refl ⟩∘⟨refl ⟩
-          (idC +₁ (u (! (coalgebras X) {A = alg now}))) ∘ [ i₁ , i₂ ∘ i₁ ] ∘ out ≈⟨ pullˡ ∘[] ⟩
-          [ (idC +₁ (u (! (coalgebras X) {A = alg now}))) ∘ i₁ 
-          , (idC +₁ (u (! (coalgebras X) {A = alg now}))) ∘ i₂ ∘ i₁ ] ∘ out      ≈⟨ []-cong₂ +₁∘i₁ (pullˡ +₁∘i₂) ⟩∘⟨refl ⟩
-          [ i₁ ∘ idC , (i₂ ∘ (u (! (coalgebras X) {A = alg now}))) ∘ i₁ ] ∘ out  ≈⟨ []-cong₂ refl assoc ⟩∘⟨refl ⟩
-          [ i₁ ∘ idC , i₂ ∘ (extend' now) ] ∘ out                                ≈˘⟨ []∘+₁ ⟩∘⟨refl ⟩
-          ([ i₁ , i₂ ] ∘ (idC +₁ extend' now)) ∘ out                             ≈⟨ elimˡ +-η ⟩∘⟨refl ⟩
-          (idC +₁ extend' now) ∘ out                                             ∎ })
-
         assoc' : ∀ {X Y Z : Obj} {g : X ⇒ D₀ Y} {h : Y ⇒ D₀ Z} → extend' (extend' h ∘ g) ≈ extend' h ∘ extend' g
         assoc' {X} {Y} {Z} {g} {h} = extend'-unique (extend' h ∘ g) (extend' h ∘ extend' g) (begin 
           out ∘ extend' h ∘ extend' g                                       ≈⟨ pullˡ (extendlaw h) ⟩

agda/src/Monad/Instance/Delay/Strong.lagda.md

@@ -88,13 +88,7 @@ module Monad.Instance.Delay.Strong {o ℓ e} (ambient : Ambient o ℓ e) (D : De
         { η = τ
         ; commute = commute' })
       ; identityˡ = identityˡ' -- triangle
-      ; η-comm = begin -- η-τ
+      ; η-comm = λ {A} {B} → τ-now (A , B)
-          τ _ ∘ (idC ⁂ now) ≈⟨ refl⟩∘⟨ (⁂-cong₂ (sym identity²) refl ○ sym ⁂∘⁂) ⟩ 
-          τ _ ∘ (idC ⁂ out⁻¹) ∘ (idC ⁂ i₁) ≈⟨ pullˡ (τ-helper _) ⟩ 
-          (out⁻¹ ∘ (idC +₁ τ _) ∘ distributeˡ⁻¹) ∘ (idC ⁂ i₁) ≈⟨ pullʳ (pullʳ distributeˡ⁻¹-i₁) ⟩ 
-          out⁻¹ ∘ (idC +₁ τ _) ∘ i₁ ≈⟨ refl⟩∘⟨ +₁∘i₁ ⟩ 
-          out⁻¹ ∘ i₁ ∘ idC ≈⟨ refl⟩∘⟨ identityʳ ⟩
-          now ∎
       ; μ-η-comm = μ-η-comm' -- μ-τ
       ; strength-assoc = strength-assoc' -- square
       }

thesis/main.tex

@@ -101,7 +101,6 @@
 \usepackage{mathpartir}
 
 \newcommand{\obj}[1]{\ensuremath{\vert \mathcal{#1} \vert}}
-
 \begin{document}
 \pagestyle{plain}
 \input{src/titlepage}%

thesis/src/01_preliminaries.tex

@@ -1,12 +1,15 @@
 \chapter{Preliminaries}
 
-We assume familiarity with basic categorical notions, in particular categories, functors, functor algebras and natural transformations.
+We assume familiarity with basic categorical notions, in particular: categories, functors, functor algebras and natural transformations, as well as special objects like (co-)products, terminal and initial objects and special morphisms like isos, epis and monos.
-Other notions that are crucial to this thesis will be introduced in this section. 
+In this chapter we will introduce notation that will be used throughout the thesis and also introduce some notions that are crucial to this thesis in more detail.
-In the following sections we will work in an ambient category that is distributive and has a parametrized natural numbers object $\mathbb{N}$.
+We write $\obj{C}$ for the objects of a category $\mathcal{C}$, $id_X$ for the identity morphism on $X$ and $(-) \circ (-)$ for the composition of morphisms. 
+We will also sometimes omit indices of the identity and of natural transformations in favor of readability.
 
 \section{Distributive and Cartesian Closed Categories}
 Let us first introduce notation for binary (co-)products by giving their usual diagrams:
 
+% TODO products bind stronger than coproducts irgendwo erwähnen
+
 \begin{figure}[ht]
 % https://q.uiver.app/#q=WzAsOCxbMiwwLCJBIFxcdGltZXMgQiJdLFswLDAsIkEiXSxbNCwwLCJCIl0sWzIsMiwiQyJdLFs4LDAsIkEgKyBCIl0sWzYsMCwiQSJdLFsxMCwwLCJCIl0sWzgsMiwiQyJdLFswLDEsIlxccGlfMSIsMl0sWzAsMiwiXFxwaV8yIl0sWzMsMiwiZyIsMl0sWzMsMSwiZiJdLFszLDAsIlxcZXhpc3RzISBcXGxhbmdsZSBmICwgZyBcXHJhbmdsZSIsMix7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImRhc2hlZCJ9fX1dLFs1LDQsImlfMSJdLFs2LDQsImlfMiIsMl0sWzUsNywiZiIsMl0sWzYsNywiZyJdLFs0LDcsIlxcZXhpc3RzICEgW2YgLCBnXSIsMV1d
 \[\begin{tikzcd}
@@ -61,7 +64,37 @@ Categories with finite products (i.e. binary products and a terminal object) are
   where $swap := \langle \pi_2 , \pi_1 \rangle : A \times B \rightarrow B \times A$.
 \end{remark}
 
-The following is the categorical abstraction of function spaces:
+\begin{proposition}
+  The distribution morphisms can be viewed as natural transformations i.e. they satisfy the following diagrams:
+% https://q.uiver.app/#q=WzAsOCxbMCwwLCJYIFxcdGltZXMgKFkgK1opIl0sWzIsMCwiQSBcXHRpbWVzIChCICsgQykiXSxbMCwxLCJYIFxcdGltZXMgWSArIFggXFx0aW1lcyBaIl0sWzIsMSwiQSBcXHRpbWVzIEIgKyBBIFxcdGltZXMgQyJdLFszLDAsIihZICsgWikgXFx0aW1lcyBYIl0sWzUsMCwiKEIgKyBDKSBcXHRpbWVzIEEiXSxbMywxLCJZIFxcdGltZXMgWCArIFogXFx0aW1lcyBYIl0sWzUsMSwiQiBcXHRpbWVzIEEgKyBDIFxcdGltZXMgQSJdLFswLDEsImYgXFx0aW1lcyAoZyArIGgpIl0sWzIsMywiZiBcXHRpbWVzIGcgKyBmIFxcdGltZXMgaCJdLFswLDIsImRzdGwiXSxbMSwzLCJkc3RsIl0sWzQsNSwiKGcgKyBoKSBcXHRpbWVzIGYiXSxbNCw2LCJkc3RyIiwyXSxbNSw3LCJkc3RyIl0sWzYsNywiZyBcXHRpbWVzIGYgKyBoIFxcdGltZXMgZiIsMl1d
+\[\begin{tikzcd}
+	{X \times (Y +Z)} && {A \times (B + C)} & {(Y + Z) \times X} && {(B + C) \times A} \\
+	{X \times Y + X \times Z} && {A \times B + A \times C} & {Y \times X + Z \times X} && {B \times A + C \times A}
+	\arrow["{f \times (g + h)}", from=1-1, to=1-3]
+	\arrow["{f \times g + f \times h}", from=2-1, to=2-3]
+	\arrow["dstl", from=1-1, to=2-1]
+	\arrow["dstl", from=1-3, to=2-3]
+	\arrow["{(g + h) \times f}", from=1-4, to=1-6]
+	\arrow["dstr"', from=1-4, to=2-4]
+	\arrow["dstr", from=1-6, to=2-6]
+	\arrow["{g \times f + h \times f}"', from=2-4, to=2-6]
+\end{tikzcd}\]
+\end{proposition}
+\begin{proof}
+  We will prove naturality of $dstl$, naturality for $dstr$ is then analogous. We use the fact that $dstl^{-1}$ is an iso and therefore also an epi.
+
+  \begin{alignat*}{1}
+    &dstl \circ (f \times (g + h)) \circ dstl^{-1}\\
+    =\;&dstl \circ (f \times (g + h)) \circ \lbrack id \times i_1 , id \times i_2 \rbrack\\
+    =\;&dstl \circ \lbrack f \times ((g + h) \circ i_1) , f \times ((g + h) \circ i_2) \rbrack\\
+    =\;&dstl \circ \lbrack f \times (i_1 \circ g) , f \times (i_2 \circ h) \rbrack\\
+    =\;&dstl \circ \lbrack id \times i_1 , id \times i_2 \rbrack \circ (f \times g + f \times h)\\
+    =\;&dstl \circ dstl^{-1} \circ (f \times g + f \times h)\\
+    =\;&(f \times g + f \times h)\\
+    =\;&(f \times g + f \times h) \circ dstl \circ dstl^{-1}
+  \end{alignat*}
+\end{proof}
+
 \begin{definition}[Exponential Object]
   % TODO introduce notation | C |
   Let $\mathcal{C}$ be a cartesian category and $X , Y \in \vert \mathcal{C} \vert$.
@@ -87,24 +120,22 @@ Monads are widely known among programmers as a way of modelling effects in pure
 
 \begin{definition}[Monad]
   A monad on a category $\mathcal{C}$ is a triple $(F, \eta, \mu)$, where $F : \mathcal{C} \rightarrow \mathcal{C}$ is an endofunctor and $\eta : Id \rightarrow F, \mu : F^2 \rightarrow F$ are natural transformations, satisfying the following laws:
-  \begin{enumerate}
+  \begin{alignat*}{1}
-    % TODO add quantifiers
+    &\mu_X \circ \mu_{FX} = \mu_X \circ F\mu_X \tag*{(M1)}\label{M1}\\
-    \item $\mu_X \circ \mu_{FX} = \mu_X \circ F\mu_X$
+    &\mu_X \circ \eta_{FX} = id_{FX} \tag*{(M2)}\label{M2}\\
-    \item $\mu_X \circ \eta_{FX} = id_{FX}$
+    &\mu_X \circ F\eta_X = id_{FX} \tag*{(M3)}\label{M3}
-    \item $\mu_X \circ F\eta_X = id_{FX}$
+  \end{alignat*}
-  \end{enumerate}
 \end{definition}
 
 For programmers a second equivalent definition is more useful:
 
 \begin{definition}[Kleisli Triple]
   A kleisli triple on a category $\mathcal{C}$ is a triple $(F, \eta, (-)^*)$, where $F : \obj{C} \rightarrow \obj{C}$ is a mapping on objects, $(\eta_X : X \rightarrow FX)_{X\in\obj{C}}$ is a family of morphisms and for every morphism $f : X \rightarrow FY$ there exists a morphism $f^* : FX \rightarrow FY$ called the kleisli lifting, where the following laws hold:
-  \begin{enumerate}
+  \begin{alignat*}{1}
-    % TODO add quantifiers
+    &\eta_X^* = id_{FX} \tag*{(K1)}\label{K1}\\
-    \item $\eta_X^* = id_{FX}$
+    &\eta_X \circ f^* = f \tag*{(K2)}\label{K2}\\
-    \item $\eta_X \circ f^* = f$
+    &f^* \circ g* = (f \circ g^*)^* \tag*{(K3)}\label{K3}
-    \item $f^* \circ g* = (f \circ g^*)^*$ 
+  \end{alignat*}
-  \end{enumerate}
 \end{definition}
 
 In functional programming languages like Haskell the Kleisli lifting $(-)^*$ is usually called \textit{bind} or written infix as \mintinline{haskell}{>>=} and $\eta$ is called $return$. Given two morphisms $f : X \rightarrow MY, g : Y \rightarrow MZ$, where $M$ is a Kleisli triple the composition $g^* \circ f$ can then be (in a pointful manner) written as \mintinline{haskell}{f x >>= g} or using Haskell's do-notation:
@@ -156,12 +187,13 @@ When modelling partiality with a monad, one would expect the following two progr
 where p and q are (partial) computations. This condition can be expressed categorically, but first we need another definition:
 
 \begin{definition}[Strong Monad] A monad $M$ on a cartesian category $\mathcal{C}$ is called strong if there exists a natural transformation $\tau_{X,Y} : X \times MY \rightarrow M(X \times Y)$, satisfying the following conditions:
-  \begin{enumerate}
+  \begin{alignat*}{1}
-  \item $M\pi_2 \circ \tau_{1,X} = \pi_2$
+    &M\pi_2 \circ \tau_{1,X} = \pi_2 \tag*{(S1)}\label{S1}\\
-  \item $M \alpha_{X,Y,Z} \circ \tau_{X \times Y, Z} = \tau_{X, Y\times Z} \circ (id_X \times \tau_{Y, Z}) \circ \alpha_{X,Y,MZ}$
+    &\tau_{X,Y} \circ (id_X \times \eta_Y) = \eta_{X\times Y} \tag*{(S2)}\label{S2}\\
-  \item $\tau_{X,Y} \circ (id_X \times \eta_Y) = \eta_{X\times Y}$
+    &\tau_{X,Y} \circ (id_X \times \mu_Y) = \mu_{X\times Y} \circ M\tau_{X,Y} \circ \tau_{X,MY} \tag*{(S3)}\label{S3}\\
-  \item $\tau_{X,Y} \circ (id_X \times \mu_Y) = \mu_{X\times Y} \circ M\tau_{X,Y} \circ \tau_{X,MY}$
+    &M \alpha_{X,Y,Z} \circ \tau_{X \times Y, Z} = \tau_{X, Y\times Z} \circ (id_X \times \tau_{Y, Z}) \circ \alpha_{X,Y,MZ} \tag*{(S4)}\label{S4}
-\end{enumerate}
+  \end{alignat*}
+where $\alpha_{X,Y,Z} : X \times (Y \times Z) \rightarrow (X \times Y) \times Z$ is the obvious associativity morphism. 
 \end{definition}
 
 Now we can express the above condition:

thesis/src/03_partiality-monads.tex

@@ -19,12 +19,12 @@ To ensure that programs are partial, we recall the following notion by Cockett a
 \newcommand{\tdom}{\text{dom}\;}
 \begin{definition}[Restriction Structure]
   A restriction structure on a category $\mathcal{C}$ is a mapping $dom : \mathcal{C}(X, Y) \rightarrow \mathcal{C}(X , X)$ with the following properties:
-  \begin{alignat}{1}
+  \begin{alignat*}{1}
-    f \circ (\tdom f) &= f\\
+    f \circ (\tdom f) &= f\tag*{(R1)}\\
-    (\tdom f) \circ (\tdom g) &= (\tdom g) \circ (\tdom f)\\
+    (\tdom f) \circ (\tdom g) &= (\tdom g) \circ (\tdom f)\tag*{(R2)}\\
-    \tdom(g \circ (\tdom f)) &= (\tdom g) \circ (\tdom f)\\
+    \tdom(g \circ (\tdom f)) &= (\tdom g) \circ (\tdom f)\tag*{(R3)}\\
-    (\tdom h) \circ f &= f \circ \tdom (h \circ f)
+    (\tdom h) \circ f &= f \circ \tdom (h \circ f)\tag*{(R4)}
-  \end{alignat}
+  \end{alignat*}
   for any $X, Y, Z \in \vert\mathcal{C}\vert, f : X \rightarrow Y, g : X \rightarrow Z, h: Y \rightarrow Z$.
 \end{definition}
 Intuitively $\tdom f$ captures the domain of definedness of $f$.
@@ -97,23 +97,152 @@ Categorically we get this monad by the final coalgebras $DX = \nu A. X + A$, whi
 
 Since $DX$ is defined as a final coalgebra, we can define morphisms via corecursion and prove theorems by coinduction. By Lambek's lemma the coalgebra structure $out : DX \rightarrow X + DX$ is an isomorphism, whose inverse can be decomposed into the two constructors mentioned before: $out^{-1} = [ now , later ] : X + DX \rightarrow DX$.
 
+\begin{corollary}
+  \label{col:delay}
+  The following conditions hold:
+  \begin{itemize}
+    \item There exists a unit morphism $\eta : X \rightarrow DX$ for any DX, satisfying 
+    \begin{equation*}
+      out \circ unit = i_1 \tag*{(D1)}\label{D1}
+    \end{equation*}
+    \item For any $f : X \rightarrow DY$ there exists a unique morphism $f^* : DX \rightarrow DY$ satisfying:
+    \begin{equation*}
+      % https://q.uiver.app/#q=WzAsNCxbMCwwLCJEWCJdLFszLDAsIlggKyBEWCJdLFswLDEsIkRZIl0sWzMsMSwiWSArIERZIl0sWzAsMSwib3V0Il0sWzAsMiwiZl4qIiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiZGFzaGVkIn19fV0sWzIsMywib3V0Il0sWzEsMywiWyBvdXQgXFxjaXJjIGYgLCBpXzIgXFxjaXJjIGZeKiBdIl1d
+      \begin{tikzcd}
+        DX &&& {X + DX} \\
+        DY &&& {Y + DY}
+        \arrow["out", from=1-1, to=1-4]
+        \arrow["{f^*}", dashed, from=1-1, to=2-1]
+        \arrow["out", from=2-1, to=2-4]
+        \arrow["{[ out \circ f , i_2 \circ f^* ]}", from=1-4, to=2-4]
+      \end{tikzcd}\tag*{(D2)}\label{D2}
+    \end{equation*}
+    \item There exists a unique morphism $\tau : X \times DY \rightarrow D(X \times Y)$ satisfying:
+    \begin{equation*}
+      % https://q.uiver.app/#q=WzAsNSxbMCwwLCJYIFxcdGltZXMgRFkiXSxbMCwxLCJEKFggXFx0aW1lcyBZKSJdLFsyLDAsIlggXFx0aW1lcyAoWSArIERZKSJdLFs0LDAsIlggXFx0aW1lcyBZICsgWCBcXHRpbWVzIERZIl0sWzQsMSwiWCBcXHRpbWVzIFkgKyBEKFggXFx0aW1lcyBZKSJdLFswLDEsIlxcdGF1IiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiZGFzaGVkIn19fV0sWzAsMiwiaWQgXFx0aW1lcyBvdXQiLDJdLFsyLDMsImRzdGwiLDJdLFszLDQsImlkICtcXHRhdSIsMl0sWzEsNCwib3V0Il1d
+      \begin{tikzcd}[ampersand replacement=\&]
+        {X \times DY} \&\& {X \times (Y + DY)} \&\& {X \times Y + X \times DY} \\
+        {D(X \times Y)} \&\&\&\& {X \times Y + D(X \times Y)}
+        \arrow["\tau", dashed, from=1-1, to=2-1]
+        \arrow["{id \times out}"', from=1-1, to=1-3]
+        \arrow["dstl"', from=1-3, to=1-5]
+        \arrow["{id +\tau}"', from=1-5, to=2-5]
+        \arrow["out", from=2-1, to=2-5]
+      \end{tikzcd}\tag*{(D3)}\label{D3}
+    \end{equation*}
+  \end{itemize}
+\end{corollary}
+\begin{proof}\;\\
+  \begin{itemize}
+    \item[\ref{D1}] Take $\eta = now$ then $out \circ now = i_1$ follows by definition of $now$.
+    \item[\ref{D2}] We define $f^* = \;! \circ i_1$, where $!$ is the unique coalgebra-morphism in this diagram:
+      % https://q.uiver.app/#q=WzAsNSxbMCwxLCJEWCArIERZIl0sWzcsMSwiWSArIChEWCArIERZKSJdLFswLDAsIkRYIl0sWzAsMiwiRFkiXSxbNywyLCJZICsgRFkiXSxbMCwxLCJbIFsgWyBpXzEgLCBpXzIgXFxjaXJjIGlfMiBdIFxcY2lyYyAob3V0IFxcY2lyYyBmKSAsIGlfMiBcXGNpcmMgaV8xIF0gXFxjaXJjIG91dCAsIChpZCArIGlfMikgXFxjaXJjIG91dCBdIl0sWzIsMCwiaV8xIl0sWzAsMywiISIsMCx7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImRhc2hlZCJ9fX1dLFszLDQsIm91dCJdLFsxLDQsImlkICsgISIsMCx7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImRhc2hlZCJ9fX1dXQ==
+      \[\begin{tikzcd}
+        DX \\
+        {DX + DY} &&&&&&& {Y + (DX + DY)} \\
+        DY &&&&&&& {Y + DY}
+        \arrow["{[ [ [ i_1 , i_2 \circ i_2 ] \circ (out \circ f) , i_2 \circ i_1 ] \circ out , (id + i_2) \circ out ]}", from=2-1, to=2-8]
+        \arrow["{i_1}", from=1-1, to=2-1]
+        \arrow["{!}", dashed, from=2-1, to=3-1]
+        \arrow["out", from=3-1, to=3-8]
+        \arrow["{id + !}", dashed, from=2-8, to=3-8]
+      \end{tikzcd}\]
+      $out \circ f^* = [ out \circ f , i_2 \circ f^* ] \circ out$ then follows from this diagram.
+
+      We are left to check uniqueness, let $g : DX \rightarrow DY$ and $out \circ g = [ out \circ f , i_2 \circ g ] \circ out$. 
+      Then $[ g , id ] : DX + DY \rightarrow DY$ is a coalgebra morphism, we get $[ g , id ] =\;!$ by uniqueness of $!$, it follows:
+      \[g = [ g , id ] \circ i_1 =\;! \circ i_1 = f^*\]
+    \item[\ref{D3}] This follows immediately, $\tau$ is the unique coalgebra morphism from $(X \times DY, dstl \circ (id \times out))$ into the terminal coalgebra $(D(X \times Y) , out)$.
+  \end{itemize}
+\end{proof}
+
 \begin{theorem}
-  $\mathbf{D}$ is a monad.
+  $\mathbf{D} = (D, now, (-)^*)$ is a kleisli triple.
 \end{theorem}
 \begin{proof}
-  We show that $\mathbf{D}$ is a kleisli triple.
+  We will use the properties proven in corollary~\ref{col:delay} to prove the kleisli triple and strength laws. 
+  First we show that $(D , now, (-)^*)$ is a kleisli triple:
+  \begin{itemize}
+    \item[\ref{K1}]
+    By uniqueness of $now^*$ it suffices to show that $out \circ id = [ out \circ now , i_2 \circ id ] \circ out$ which instantly follows by \ref{D1}.
+    \item[\ref{K2}] Let $f : X \rightarrow DY$, we use the fact that $out$ is monic:
     
-  Choose $now : X \rightarrow DX$ and given $f : X \rightarrow DY$ we define $f^* =\; ! \circ i_1$ by:
+    \[out \circ f^* \circ now \overset{\ref{D2}}{=} [ out \circ f , i_2 \circ f^* ] \circ out \circ now \overset{\ref{D1}}{=} out \circ f \]
     
-  % https://q.uiver.app/#q=WzAsNSxbMCwxLCJEWCArIERZIl0sWzYsMSwiWSArIChEWCArIERZKSJdLFswLDAsIkRYIl0sWzAsMiwiRFkiXSxbNiwyLCJZICsgRFkiXSxbMCwxLCJbIFsgWyBp4oKBICwgaeKCgiDiiJggaeKCgiBdIOKImCAob3V0IOKImCBmKSAsIGnigoIg4oiYIGnigoEgXSDiiJggb3V0ICwgKGlkQyAr4oKBIGnigoIpIOKImCBvdXQgXSJdLFsyLDAsImlfMSJdLFswLDMsIiEiLDAseyJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJkYXNoZWQifX19XSxbMyw0LCJvdXQiXSxbMSw0LCJGICEiLDAseyJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJkYXNoZWQifX19XV0=
+    \item[\ref{K3}] Using uniqueness of $(h^* \circ g)^*$ we need to show $out \circ h^* \circ g^* = [ out \circ h^* \circ g , i_2 \circ h^* \circ g^* ] \circ out$ which follows by multiple uses of \ref{D2}.
-  \[\begin{tikzcd}
+  \end{itemize}
-    DX \\
+\end{proof}
-    {DX + DY} &&&&&& {Y + (DX + DY)} \\
+
-    DY &&&&&& {Y + DY}
+Since $DX$ is a final coalgebra we get the following proof principle:
-    \arrow["{[ [ [ i_1 , i_2 \circ i_2 ] \circ (out \circ f) , i_2 \circ i_1 ] \circ out , (id +₁ i_2) \circ out ]}", from=2-1, to=2-7]
+\begin{remark}[Proof by coinduction]
-    \arrow["{i_1}", from=1-1, to=2-1]
+  \label{rem:coinduction}
-    \arrow["{!}", dashed, from=2-1, to=3-1]
+  Given two morphisms $f, g : X \rightarrow DY$.
-    \arrow["out", from=3-1, to=3-7]
+  To show that $f = g$ it suffices to show that there exists a coalgebra structure $\alpha : X \rightarrow Y + X$ such that the following diagrams commute:
-    \arrow["{F !}", dashed, from=2-7, to=3-7]
+  % https://q.uiver.app/#q=WzAsOCxbMCwwLCJYIl0sWzAsMSwiRFkiXSxbMiwxLCJZICsgRFkiXSxbMiwwLCJZICsgWCJdLFs0LDAsIlgiXSxbNCwxLCJEWSJdLFs2LDAsIlkgKyBYIl0sWzYsMSwiWSArIERZIl0sWzEsMiwib3V0Il0sWzAsMywiXFxhbHBoYSJdLFswLDEsImYiXSxbMywyLCJpZCArIGYiXSxbNCw2LCJcXGFscGhhIl0sWzQsNSwiZyJdLFs2LDcsImlkICsgZyJdLFs1LDcsIm91dCIsMl1d
-  \end{tikzcd}\]
+  \[\begin{tikzcd}
+    X && {Y + X} && X && {Y + X} \\
+    DY && {Y + DY} && DY && {Y + DY}
+    \arrow["out", from=2-1, to=2-3]
+    \arrow["\alpha", from=1-1, to=1-3]
+    \arrow["f", from=1-1, to=2-1]
+    \arrow["{id + f}", from=1-3, to=2-3]
+    \arrow["\alpha", from=1-5, to=1-7]
+    \arrow["g", from=1-5, to=2-5]
+    \arrow["{id + g}", from=1-7, to=2-7]
+    \arrow["out"', from=2-5, to=2-7]
+  \end{tikzcd}\]
+  Uniqueness of the coalgebra morphism $! : (X, \alpha) \rightarrow (DY, out)$ then gives us that indeed $f = g$.
+\end{remark}
+
+\begin{theorem}
+  $\mathbf{D}$ is a strong monad.
+\end{theorem}
+\begin{proof}
+  Most of the following proofs are done via coinduction (remark~\ref{rem:coinduction}), we will only give the needed coalgebra structure, the proofs that the diagrams commute can be looked up in the agda formalization.
+
+  First we need to show naturality of $\tau$, i.e. we need to show that 
+  \[\tau \circ (f \times (now \circ g)^*) = (now \circ (f \times g))^* \circ \tau\]
+  The needed coalgebra is shown in this diagram:
+  % https://q.uiver.app/#q=WzAsNixbMCwwLCJYIFxcdGltZXMgRFkiXSxbMCwyLCJEKEFcXHRpbWVzIEIpIl0sWzQsMiwiQVxcdGltZXMgQiArIEQoQSBcXHRpbWVzIEIpIl0sWzEsMCwiWCBcXHRpbWVzIChZICsgRFkpIl0sWzIsMCwiWCBcXHRpbWVzIFkgKyBYIFxcdGltZXMgRFkiXSxbNCwwLCJBIFxcdGltZXMgQiArIFggXFx0aW1lcyBEWSJdLFsxLDIsIm91dCJdLFswLDMsImlkIFxcdGltZXMgb3V0Il0sWzMsNCwiZHN0bCJdLFswLDEsIiEiLDAseyJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJkYXNoZWQifX19XSxbNCw1LCJmIFxcdGltZXMgZyArIGlkIl0sWzUsMiwiaWQgKyAhIiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiZGFzaGVkIn19fV1d
+  \[\begin{tikzcd}
+    {X \times DY} & {X \times (Y + DY)} & {X \times Y + X \times DY} && {A \times B + X \times DY} \\
+    \\
+    {D(A\times B)} &&&& {A\times B + D(A \times B)}
+    \arrow["out", from=3-1, to=3-5]
+    \arrow["{id \times out}", from=1-1, to=1-2]
+    \arrow["dstl", from=1-2, to=1-3]
+    \arrow["{!}", dashed, from=1-1, to=3-1]
+    \arrow["{f \times g + id}", from=1-3, to=1-5]
+    \arrow["{id + !}", dashed, from=1-5, to=3-5]
+  \end{tikzcd}\]
+  Next we check the strength laws:
+  \begin{itemize}
+    \item[\ref{S1}] To show that $(now \circ \pi_2)^* \circ \tau = \pi_2$ we take the following coalgebra:
+      % https://q.uiver.app/#q=WzAsNixbMCwwLCIxIFxcdGltZXMgRFgiXSxbMCwxLCJEWCJdLFs1LDAsIlggKyAxIFxcdGltZXMgRFgiXSxbNSwxLCJYICsgRFgiXSxbMiwwLCIxIFxcdGltZXMgWCArIERYIl0sWzMsMCwiMSBcXHRpbWVzIFggKyAxIFxcdGltZXMgRFgiXSxbMSwzLCJvdXQiXSxbMCwxLCIhIiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiZGFzaGVkIn19fV0sWzIsMywiaWQgKyAhIl0sWzAsNCwiaWQgXFx0aW1lcyBvdXQiXSxbNCw1LCJkc3RsIl0sWzUsMiwiXFxwaV8yICsgaWQiXV0=
+      \[\begin{tikzcd}
+        {1 \times DX} && {1 \times X + DX} & {1 \times X + 1 \times DX} && {X + 1 \times DX} \\
+        DX &&&&& {X + DX}
+        \arrow["out", from=2-1, to=2-6]
+        \arrow["{!}", dashed, from=1-1, to=2-1]
+        \arrow["{id + !}", from=1-6, to=2-6]
+        \arrow["{id \times out}", from=1-1, to=1-3]
+        \arrow["dstl", from=1-3, to=1-4]
+        \arrow["{\pi_2 + id}", from=1-4, to=1-6]
+      \end{tikzcd}\]
+    \item[\ref{S2}] To show that $\tau \circ (id \times now) = now$ we don't need coinduction, but we need a small helper lemma:
+    \begin{equation*}
+      \tau \circ (id \times out^{-1}) = out^{-1} \circ (id + \tau) \circ dstl \tag*{($\ast$)}\label{helper}
+    \end{equation*}
+    which is a direct consequence of \ref{D3}.
+    With this the proof is straightforward:
+    \begin{alignat*}{1}
+      &\tau \circ (id \times now)\\
+      =\;&\tau \circ (id \times out^{-1}) \circ (id \times i_1)\\
+      =\;&out^{-1} \circ (id + \tau) \circ dstl \circ (id \times i_1)\tag*{\ref*{helper}}\\
+      =\;&now
+    \end{alignat*}
+    where the last step follows since $dstl \circ (id \times i_1) = i_1$.
+    \item[\ref{S3}]
+    \item[\ref{S4}]
+  \end{itemize}
 \end{proof}