improve proves in delay chapter

thesis/src/01_preliminaries.tex

@@ -8,7 +8,7 @@ We write $\obj{C}$ for the objects of a category $\C$, $id_X$ for the identity m
 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:
+Let us first introduce notation for binary (co-) products by giving their usual diagrams:
 
 \begin{figure}[ht]
 % https://q.uiver.app/#q=WzAsOCxbMiwwLCJBIFxcdGltZXMgQiJdLFswLDAsIkEiXSxbNCwwLCJCIl0sWzIsMiwiQyJdLFs4LDAsIkEgKyBCIl0sWzYsMCwiQSJdLFsxMCwwLCJCIl0sWzgsMiwiQyJdLFswLDEsIlxccGlfMSIsMl0sWzAsMiwiXFxwaV8yIl0sWzMsMiwiZyIsMl0sWzMsMSwiZiJdLFszLDAsIlxcZXhpc3RzISBcXGxhbmdsZSBmICwgZyBcXHJhbmdsZSIsMix7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImRhc2hlZCJ9fX1dLFs1LDQsImlfMSJdLFs2LDQsImlfMiIsMl0sWzUsNywiZiIsMl0sWzYsNywiZyJdLFs0LDcsIlxcZXhpc3RzICEgW2YgLCBnXSIsMV1d
@@ -34,10 +34,9 @@ We will furthermore overload this notation and write $f \times g := \langle f \c
 
 We write $1$ for the terminal object together with the unique morphism $! : A \rightarrow 1$ and $0$ for the initial object with the unique morphism $\text{!`} : A \rightarrow 0$.
 
-Categories with finite products (i.e. binary products and a terminal object) are also called cartesian and categories with finite coproducts (i.e. binary coproducts and an initial object) are called cocartesian.
+Categories with finite products (i.e.\ binary products and a terminal object) are also called cartesian and categories with finite coproducts (i.e. binary coproducts and an initial object) are called cocartesian.
 
-\begin{definition}[Distributive Category]
+\begin{definition}[Distributive Category]~\label{def:distributive}
-  \label{def:distributive}
   A cartesian and cocartesian category $\C$ is called distributive if the canonical (left) distributivity morphism $dstl^{-1}$ is an iso:
   % https://q.uiver.app/#q=WzAsMixbMCwwLCJYIFxcdGltZXMgWSArIFggXFx0aW1lcyBaIl0sWzMsMCwiWCBcXHRpbWVzIChZICsgWikiXSxbMCwxLCJkc3RsXnstMX0gOj0ge1xcbGJyYWNrIGlkIFxcdGltZXMgaV8xICwgaWQgXFx0aW1lcyBpXzIgXFxyYnJhY2t9IiwwLHsiY3VydmUiOi0zfV0sWzEsMCwiZHN0bCIsMCx7ImN1cnZlIjotM31dXQ==
   \[\begin{tikzcd}
@@ -65,7 +64,7 @@ Categories with finite products (i.e. binary products and a terminal object) are
 \end{remark}
 
 \begin{proposition}
-  The distribution morphisms can be viewed as natural transformations i.e. they satisfy the following diagrams:
+  The distribution morphisms can be viewed as natural transformations i.e.\ they satisfy the following diagrams:
   % https://q.uiver.app/#q=WzAsOCxbMCwwLCJYIFxcdGltZXMgKFkgK1opIl0sWzIsMCwiQSBcXHRpbWVzIChCICsgQykiXSxbMCwxLCJYIFxcdGltZXMgWSArIFggXFx0aW1lcyBaIl0sWzIsMSwiQSBcXHRpbWVzIEIgKyBBIFxcdGltZXMgQyJdLFszLDAsIihZICsgWikgXFx0aW1lcyBYIl0sWzUsMCwiKEIgKyBDKSBcXHRpbWVzIEEiXSxbMywxLCJZIFxcdGltZXMgWCArIFogXFx0aW1lcyBYIl0sWzUsMSwiQiBcXHRpbWVzIEEgKyBDIFxcdGltZXMgQSJdLFswLDEsImYgXFx0aW1lcyAoZyArIGgpIl0sWzIsMywiZiBcXHRpbWVzIGcgKyBmIFxcdGltZXMgaCJdLFswLDIsImRzdGwiXSxbMSwzLCJkc3RsIl0sWzQsNSwiKGcgKyBoKSBcXHRpbWVzIGYiXSxbNCw2LCJkc3RyIiwyXSxbNSw3LCJkc3RyIl0sWzYsNywiZyBcXHRpbWVzIGYgKyBoIFxcdGltZXMgZiJdXQ==
   \[\begin{tikzcd}[column sep=4ex]
     {X \times (Y +Z)} && {A \times (B + C)} & {(Y + Z) \times X} && {(B + C) \times A} \\
@@ -81,7 +80,7 @@ Categories with finite products (i.e. binary products and a terminal object) are
   \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.
+  We will prove naturality of $dstl$, naturality for $dstr$ is symmetric. 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}\\
@@ -95,6 +94,65 @@ Categories with finite products (i.e. binary products and a terminal object) are
   \end{alignat*}
 \end{proof}
 
+\begin{proposition}
+  The distribution morphisms satisfy the following equations:
+
+  \begin{alignat}{2}
+    &dstl \circ (id \times i_1) &&= i_1
+    \\&dstl \circ (id \times i_2) &&= i_2
+    \\&[ \pi_1 , \pi_1 ] \circ dstl &&= \pi_1
+    \\&( \pi_2 + \pi_2 ) \circ dstl &&= \pi_2
+    \\&dstl \circ swap &&= (swap + swap) \circ dstr
+    \\&dstr \circ (i_1 \times id) &&= i_1
+    \\&dstr \circ (i_2 \times id) &&= i_2
+    \\&(\pi_1 + \pi_1) \circ dstr &&= \pi_1
+    \\&[ \pi_2 , \pi_2 ] \circ dstr &&= \pi_2
+    \\&dstr \circ swap &&= (swap + swap) \circ dstl
+  \end{alignat}
+\end{proposition}
+\begin{proof}
+  Let us verify the five equations concerning $dstl$, the ones concerning $dstr$ follow symmetrically:
+
+  \begin{alignat*}{1}
+    &dstl \circ (id \times i_1)
+    \\=\;&dstl \circ [ id \times i_1 , id \times i_2 ] \circ i_1
+    \\=\;&dstl \circ dstl^{-1} \circ i_1
+    \\=\;&i_1
+  \end{alignat*}
+
+  \begin{alignat*}{1}
+    &dstl \circ (id \times i_2)
+    \\=\;&dstl \circ [ id \times i_1 , id \times i_2 ] \circ i_2
+    \\=\;&dstl \circ dstl^{-1} \circ i_2
+    \\=\;&i_2
+  \end{alignat*}
+
+  The next two follow by the fact that $dstl^{-1}$ is epic:
+
+  \begin{alignat*}{1}
+    &\pi_1 \circ dstl^{-1}
+    \\=\;&[ \pi_1 \circ (id \times i_1) , \pi_1 \circ (id \times i_2) ]
+    \\=\;&[ \pi_1 , \pi_1 ]
+  \end{alignat*}
+
+  \begin{alignat*}{1}
+    &\pi_2 \circ dstl^{-1}
+    \\=\;& [ \pi_2 \circ (id \times i_1) , \pi_2 \circ (id \times i_2) ]
+    \\=\;& \pi_2 + \pi_2
+  \end{alignat*}
+
+  And by monicity of $dstl^{-1}$:
+
+  \begin{alignat*}{1}
+    &dstl^{-1} \circ (swap + swap) \circ dstl
+    \\=\;&[ (id \times i_1) \circ swap, (id \times i_2) \circ swap ] \circ dstl
+    \\=\;&[ swap \circ (i_1 \times id) , swap \circ (i_2 \times id) ] \circ dstl
+    \\=\;&swap \circ dstl^{-1} \circ dstl
+    \\=\;&swap
+  \end{alignat*}
+
+\end{proof}
+
 \begin{definition}[Exponential Object]
   Let $\C$ be a cartesian category and $X , Y \in \vert \C \vert$.
   An object $X^Y$ is called an exponential object (of $X$ and $Y$) if there exists an evaluation morphism $eval : X^Y \times Y \rightarrow X$ and for any $f : X \times Y \rightarrow Z$ there exists a morphism $curry\; f : X \rightarrow Z^Y$ that is unique with respect to the following diagram:

thesis/src/03_partiality-monads.tex

@@ -113,15 +113,22 @@ The endofunctor $MX = X + 1$ extends to a monad by taking $\eta_X = i_1 : X \rig
       \arrow["{id+\;!}", from=3-4, to=5-4]
       \arrow["{\langle i_1,id\rangle + \;!}"', from=1-1, to=5-4]
     \end{tikzcd}\]
-  By pre-composing with $i_1$ and $i_2$ it suffices to show that
+
-  \[i_1 \circ \langle i_1 , id \rangle = (id\;+\;!) \circ dstl \circ \langle i_1 , i_1 \rangle\]
+  This is easily proven by pre-composing with $i_1$ and $i_2$:
-  and
+  \begin{alignat*}{1}
-  \[i_2 \;\circ \;! = (id\;+\;!) \circ dstl \circ \langle i_2 , i_2 \rangle\]
+    &(id\;+\;!) \circ dstl \circ \langle i_1 , i_1 \rangle
-  which follow easily by the facts that
+    \\=\;&(id\;+\;!) \circ dstl \circ (id \times i_1) \circ \langle i_1 , id \rangle
-  \[dstl \circ (id \times i_1) = i_1\]
+    \\=\;&(id\;+\;!) \circ i_1 \circ \langle i_1 , id \rangle
-  and
+    \\=\;&i_1 \circ \langle i_1 , id \rangle
-  \[dstl \circ (id \times i_2) = i_2\]
+  \end{alignat*}
-  that are both proven by monicity of $dstl^{-1}$.
+
+  \begin{alignat*}{1}
+    &(id\;+\;!) \circ dstl \circ \langle i_2 , i_2 \rangle
+    \\=\;&(id\;+\;!) \circ dstl \circ (id \times i_2) \circ \langle i_2 , id \rangle
+    \\=\;&(id\;+\;!) \circ i_2 \circ \langle i_2 , id \rangle
+    \\=\;&i_2 \;\circ\; ! \circ \langle i_2 , id \rangle
+    \\=\;&i_2 \;\circ\; !
+  \end{alignat*}
 \end{proof}
 
 In the setting of classical mathematics this monad is therefore sufficient for modelling partiality, but in general it will not be useful for modelling  non-termination as a side effect, since one would need to know beforehand whether a program terminates or not. For the purpose of modelling possibly non-terminating computations another monad has been developed by Capretta~\cite{delay}.
@@ -141,13 +148,12 @@ Categorically we obtain this monad by the final coalgebras $DX = \nu A. X + A$,
 
 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{proposition}
+\begin{proposition}~\label{col:delay}
-  \label{col:delay}
   The following conditions hold:
   \begin{itemize}
-    \item There exists a unit morphism $now : X \rightarrow DX$ for any DX, satisfying
+    \item $now : X \rightarrow DX$ and $later : DX \rightarrow DX$ satisfy:
           \begin{equation*}
-            out \circ now = i_1 \tag*{(D1)}\label{D1}
+            out \circ now = i_1 \qquad\qquad\qquad out \circ later = i_2 \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*}
@@ -179,7 +185,11 @@ Since $DX$ is defined as a final coalgebra, we can define morphisms via corecurs
 \begin{proof}
   We will make use of the fact that every $DX$ is a final coalgebra:
   \begin{itemize}
-    \item[\ref{D1}] This follows by definition of $now$.
+    \item[\ref{D1}] These follow by definition:
+    \begin{alignat*}{3}
+      &out \circ now &&= out \circ out^{-1} \circ i_1 &= i_1
+      \\&out \circ later &&= out \circ out^{-1} \circ i_2 &= i_2
+    \end{alignat*}
     \item[\ref{D2}] We define $f^* = \;\coalg{\alpha} \circ i_1$, where $\coalg{\alpha}$ is the unique coalgebra morphism in this diagram:
 
           % https://q.uiver.app/#q=WzAsNSxbMCwxLCJEWCArIERZIl0sWzcsMSwiWSArIChEWCArIERZKSJdLFswLDAsIkRYIl0sWzAsMiwiRFkiXSxbNywyLCJZICsgRFkiXSxbMCwxLCJcXGFscGhhIDo9IFsgWyBbIGlfMSAsIGlfMiBcXGNpcmMgaV8yIF0gXFxjaXJjIChvdXQgXFxjaXJjIGYpICwgaV8yIFxcY2lyYyBpXzEgXSBcXGNpcmMgb3V0ICwgKGlkICsgaV8yKSBcXGNpcmMgb3V0IF0iXSxbMiwwLCJpXzEiXSxbMCwzLCJcXGNvYWxne1xcYWxwaGF9IiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiZGFzaGVkIn19fV0sWzMsNCwib3V0Il0sWzEsNCwiaWQgKyBcXGNvYWxne1xcYWxwaGF9IiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiZGFzaGVkIn19fV1d
@@ -193,12 +203,39 @@ Since $DX$ is defined as a final coalgebra, we can define morphisms via corecurs
               \arrow["out", from=3-1, to=3-8]
               \arrow["{id + \coalg{\alpha}}", 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.
 
-          \improvement{Details of why it is coalgebra morphism}
+          Note that $\coalg{\alpha} \circ i_2 = id : (DY, out) \rightarrow (DY, out)$, by uniqueness of the identity morphism and the fact that $\coalg{\alpha} \circ i_2$ is a coalgebra morphism:
+          \begin{alignat*}{1}
+            &out \circ \coalg{\alpha} \circ i_2
+            \\=\;&(id+\coalg{\alpha}) \circ \alpha \circ i_2
+            \\=\;&(id + \coalg{\alpha}) \circ (id + i_2) \circ out
+            \\=\;&(id + \coalg{\alpha} \circ i_2) \circ out
+          \end{alignat*}
+          Let us verify that $f^*$ indeed satisfies the requisite property:
 
-          We are left to check uniqueness. Let $g : DX \rightarrow DY$ and $out \circ g = [ out \circ f , i_2 \circ g ] \circ out$.
+          \begin{alignat*}{1}
-          Then $[ g , id ] : DX + DY \rightarrow DY$ is a coalgebra morphism and thus $[ g , id ] =\;\coalg{\alpha}$ by uniqueness of $\coalg{\alpha}$.
+            &out \circ \coalg{\alpha} \circ i_1
+            \\=\;&(id + \coalg{\alpha}) \circ \alpha \circ i_1
+            \\=\;&(id + \coalg{\alpha}) \circ [ [ i_1 , i_2 \circ i_2 ] \circ out \circ f , i_2 \circ i_1 ] \circ out
+            \\=\;&[ [ (id + \coalg{\alpha}) \circ i_1 , (id + \coalg{\alpha}) \circ i_2 \circ i_2 ] \circ out \circ f , (id + \coalg{\alpha}) \circ i_2 \circ i_1 ] \circ out
+            \\=\;&[ [ i_1 , i_2 \circ \coalg{\alpha} \circ i_2 ] \circ out \circ f , i_2 \circ \coalg{\alpha} \circ i_1 ] \circ out
+            \\=\;&[ out \circ f , i_2 \circ f^* ] \circ out
+          \end{alignat*}
+
+          We are left to check uniqueness of $f^*$. Let $g : DX \rightarrow DY$ and $out \circ g = [ out \circ f , i_2 \circ g ] \circ out$.
+          Note that $[ g , id ] : DX + DY \rightarrow DY$ is a coalgebra morphism:
+          \begin{alignat*}{1}
+            &out \circ [ g , id ]
+            \\=\;&[ out \circ g , out ]
+            \\=\;&[ [ out \circ f , i_2 \circ g ] \circ out , out]
+            \\=\;&[ [ [ i_1 , i_2 ] \circ out \circ f , i_2 \circ g ] \circ out , (id + id) \circ out ]
+            \\=\;&[ [ [ i_1 , i_2 \circ [g , id] \circ i_2 ] \circ out \circ f , i_2 \circ [g , id] \circ i_1 ] \circ out , (id + [g , id] \circ i_2) \circ out ]
+            \\=\;&[ [ [ (id + [g , id]) \circ i_1 , (id + [g , id]) \circ i_2 \circ i_2 ] \circ out \circ f , (id + [g , id]) \circ i_2 \circ i_1 ] \circ out 
+            \\\;&, (id + [g , id]) \circ (id + i_2) \circ out ]
+            \\=\;&(id + [g , id]) \circ [ [ [ i_1 , i_2 \circ i_2 ] \circ out \circ f , i_2 \circ i_1 ] \circ out , (id + i_2) \circ out ]
+          \end{alignat*}
+
+          Thus, $[ g , id ] = \coalg{\alpha}$ by uniqueness of $\coalg{\alpha}$.
           It follows: \[g = [ g , id ] \circ i_1 =\;\coalg{\alpha} \circ i_1 = f^*\]
     \item[\ref{D3}] This follows immediately since $\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}
@@ -231,8 +268,7 @@ Since $DX$ is defined as a final coalgebra, we can define morphisms via corecurs
 \end{proof}
 
 Finality of the coalgebras $(DX, out : DX \rightarrow X + DX)_{X \in \obj{\C}}$ yields the following proof principle:
-\begin{remark}[Proof by coinduction]
+\begin{remark}[Proof by coinduction]~\label{rem:coinduction}
-  \label{rem:coinduction}
   Given two morphisms $f, g : X \rightarrow DY$. 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:
   % https://q.uiver.app/#q=WzAsOCxbMCwwLCJYIl0sWzAsMSwiRFkiXSxbMiwxLCJZICsgRFkiXSxbMiwwLCJZICsgWCJdLFs0LDAsIlgiXSxbNCwxLCJEWSJdLFs2LDAsIlkgKyBYIl0sWzYsMSwiWSArIERZIl0sWzEsMiwib3V0Il0sWzAsMywiXFxhbHBoYSJdLFswLDEsImYiXSxbMywyLCJpZCArIGYiXSxbNCw2LCJcXGFscGhhIl0sWzQsNSwiZyJdLFs2LDcsImlkICsgZyJdLFs1LDcsIm91dCJdXQ==
   \[\begin{tikzcd}[ampersand replacement=\&]
@@ -271,7 +307,7 @@ Finality of the coalgebras $(DX, out : DX \rightarrow X + DX)_{X \in \obj{\C}}$
       \arrow["{f \times g + id}", from=1-3, to=1-5]
       \arrow["{id + \coalg{-}}", dashed, from=1-5, to=3-5]
     \end{tikzcd}\]
-  We write $\coalg{-}$ to abbreviate the used coalgebra, i.e. in this diagram $\coalg{-} = \coalg{(f\times g + id) \circ dstl \circ (id \times out)}$
+  We write $\coalg{-}$ to abbreviate the used coalgebra, i.e.\ in this diagram $\coalg{-} = \coalg{(f\times g + id) \circ dstl \circ (id \times out)}$
 
   Next we check the strength laws:
   \begin{itemize}
@@ -369,11 +405,12 @@ To prove that $\mathbf{D}$ is commutative we will use another proof principle pr
 Let us record some facts that we will use to prove commutativity of $\mathbf{D}$:
 
 \begin{corollary}
-  The following two properties hold:
+  The following properties hold:
-  \begin{alignat*}{1}
+  \begin{alignat}{1}
-    &out \circ Df = (f + Df) \circ out
+    &out \circ Df = (f + Df) \circ out\label{eq:outD}
-    \\&later \circ f^* = (later \circ f)^* = f^* \circ later
+    \\&f^* = [ f , {(later \circ f)}^* ] \circ out\label{eq:f*help}
-  \end{alignat*}
+    \\&later \circ f^* = {(later \circ f)}^* = f^* \circ later\label{eq:later*}
+  \end{alignat}
 
   As well as these properties of $\tau$ and $\sigma$:
   \begin{alignat*}{2}
@@ -385,37 +422,65 @@ Let us record some facts that we will use to prove commutativity of $\mathbf{D}$
 \end{corollary}
 
 \begin{proof}
-  Let us start with the first two properties:
+  We prove them one by one:
-
-  \begin{alignat*}{1}
-    &out \circ Df
-    \\=\;&out \circ (now \circ f)^*
-    \\=\;&[ out \circ now \circ f , i_2 \circ (now \circ f)^* ] \circ out\tag*{\ref{D2}}
-    \\=\;&(f + Df) \circ out\tag*{\ref{D1}}
-  \end{alignat*}
-
-  \begin{alignat*}{1}
-    &(later \circ f)^*
-    % ... TODO
-    \\=\;&later \circ f^*
-    % ... TODO
-    \\=\;&f^* \circ later
-  \end{alignat*}
 
   \begin{itemize}
-    \item[\ref{tau1}] This is just \ref{D3} restated.
+    \item[(\ref{eq:outD})] Note that $Df = {(now \circ f)}^*$ definitionally for any $f : X \rightarrow TY$. This is then simply a consequence of~\ref*{D2}.
-    \item[\ref{sigma1}]
-          \todo[inline]{What to do about out-law?}
     \begin{alignat*}{1}
-             & out \circ Dswap \circ \tau \circ swap
+      &out \circ Df
-            \\=\;&(swap + Dswap) \circ out \circ \tau \circ swap
+      \\=\;&out \circ {(now \circ f)}^*
+      \\=\;&[ out \circ now \circ f , i_2 \circ {(now \circ f)}^* ] \circ out\tag*{\ref{D2}}
+      \\=\;&(f + Df) \circ out\tag*{\ref{D1}}
+    \end{alignat*}
+    \item[(\ref{eq:f*help})] By uniqueness of $f^*$ it suffices to show:
+    \begin{alignat*}{1}
+      &out \circ [ f , {(later \circ f)}^* ] \circ out
+      \\=\;&[ out \circ f , out \circ {(later \circ f)}^* ] \circ out
+      \\=\;&[out \circ f , [ out \circ later \circ f , i_2 \circ {(later \circ f)}^* ] \circ out ] \circ out\tag*{\ref{D2}}
+      \\=\;&[out \circ f , i_2 \circ [ f , {(later \circ f)}^* ] \circ out ] \circ out\tag*{\ref{D1}}
+    \end{alignat*}
+    \item[(\ref{eq:later*})] 
+    The next one follows by monicity of $out$:
+
+    \begin{alignat*}{1}
+      &out \circ {(later \circ f)}^*
+      \\=\;&[ out \circ later \circ f , i_2 \circ {(later \circ f)}^*] \circ out\tag*{\ref{D2}}
+      \\=\;&i_2 \circ [ f , {(later \circ f)}^*] \circ out\tag*{\ref{D1}}
+      \\=\;&i_2 \circ f^*\tag*{(\ref{eq:f*help})}
+      \\=\;&out \circ later \circ f^*\tag*{\ref{D1}}
+      \\=\;&i_2 \circ f^*\tag*{\ref{D1}}
+      \\=\;&[ out \circ f , i_2 \circ f^* ] \circ i_2
+      \\=\;&[ out \circ f , i_2 \circ f^* ] \circ out \circ later\tag*{\ref{D1}}
+      \\=\;&out \circ f^* \circ later \tag*{\ref{D2}}
+    \end{alignat*}
+  \end{itemize}
+
+
+
+  \begin{itemize}
+    \item[\ref{tau1}] This is just~\ref{D3} restated.
+    \item[\ref{sigma1}]
+      \begin{alignat*}{1}
+        &out \circ \sigma
+        \\=\;&out \circ Dswap \circ \tau \circ swap
+        \\=\;&(swap + Dswap) \circ out \circ \tau \circ swap\tag*{(\ref{eq:outD})}
         \\=\;&(swap + Dswap) \circ (id + \tau) \circ dstl \circ (id \times out) \circ swap \tag*{\ref{tau1}}
         \\=\;&(swap + Dswap) \circ (id + \tau) \circ dstl \circ swap \circ (out \times id)
         \\=\;&(swap + Dswap) \circ (id + \tau) \circ (swap + swap) \circ dstr \circ (out \times id)
         \\=\;&(id + \sigma) \circ dstr \circ (out \times id)
       \end{alignat*}
-    \item[\ref{tau2}]
+    \item[\ref{tau2}] By monicity of $out$:
-    \item[\ref{sigma2}]
+      \begin{alignat*}{1}
+        &out \circ \tau \circ (id \times out^{-1})
+        \\=\;&(id + \tau) \circ dstl \circ (id \times out) \circ (id \times out^{-1})\tag*{\ref{tau1}}
+        \\=\;&(id + \tau) \circ dstl
+      \end{alignat*}
+    \item[\ref{sigma2}] By monicity of $out$:
+      \begin{alignat*}{1}
+        &out \circ \sigma \circ (out^{-1} \times id)
+        \\=\;&(id + \sigma) \circ dstr \circ (out \times id) \circ (out^{-1} \times id)\tag*{\ref{sigma1}}
+        \\=\;&(id + \sigma) \circ dstr
+      \end{alignat*}
   \end{itemize}
 \end{proof}
 
@@ -423,7 +488,7 @@ Let us record some facts that we will use to prove commutativity of $\mathbf{D}$
   $\mathbf{D}$ is commutative.
 \end{theorem}
 \begin{proof}
-  Using corollary~\ref{cor:solution} it suffices to show that both $\tau^* \circ \sigma$ and $\sigma^* \circ \tau$ are solutions of some guarded morphism $g$.
+  Using \autoref{cor:solution} it suffices to show that both $\tau^* \circ \sigma$ and $\sigma^* \circ \tau$ are solutions of some guarded morphism $g$.
 
   Let $w = (dstr + dstr) \circ dstl \circ (out \times out)$ and take
   \[g = out^{-1} \circ [ i_1 + D i_1 \circ \sigma , i_2 \circ [ D i_1 \circ \tau , later \circ now \circ i_2 ] ] \circ w\]
@@ -436,30 +501,14 @@ Let us record some facts that we will use to prove commutativity of $\mathbf{D}$
 
   The last step in both equations holds generally for any $f : DX \times DY \rightarrow D(X \times Y)$ by monicity of $out$:
   \begin{alignat*}{1}
-        & out \circ [ now , f ]^* \circ out^{-1} \circ [ i_1 + D i_1 \circ \sigma , i_2 \circ [ D i_1 \circ \tau , later \circ now \circ i_2 ] ] \circ w                             \\
+        & out \circ {[ now , f ]}^* \circ out^{-1} \circ [ i_1 + D i_1 \circ \sigma , i_2 \circ [ D i_1 \circ \tau , later \circ now \circ i_2 ] ] \circ w
-    =\; & [ out \circ [ now , f ] , i_2 \circ [ now , f ]^* ] \circ [ i_1 + D i_1 \circ \sigma , i_2 \circ [ D i_1 \circ \tau , later \circ now \circ i_2 ] ] \circ w\tag*{\ref{D2}} \\
+    \\=\; & [ out \circ [ now , f ] , i_2 \circ {[ now , f ]}^* ] \circ [ i_1 + D i_1 \circ \sigma , i_2 \circ [ D i_1 \circ \tau , later \circ now \circ i_2 ] ] \circ w\tag*{\ref{D2}}
-    =\; & [ id + \sigma , i_2 \circ [ now , f]^* \circ [ D i_1 \circ \tau , later \circ now \circ i_2 ] ] \circ w\tag*{\ref{D1}}                                                     \\
+    \\=\; & [ id + \sigma , i_2 \circ {[ now , f]}^* \circ [ D i_1 \circ \tau , later \circ now \circ i_2 ] ] \circ w\tag*{\ref{D1}}
-    =\; & [ id + \sigma , i_2 \circ [ \tau , [ now , f]^* \circ later \circ now \circ i_2 ] ] \circ w                                                                                \\
+    \\=\; & [ id + \sigma , i_2 \circ [ \tau , {[ now , f]}^* \circ later \circ now \circ i_2 ] ] \circ w
-    =\; & [ id + \sigma , i_2 \circ [ \tau , [ later \circ now , later \circ f]^* \circ now \circ i_2 ] ] \circ w                                                                    \\
+    \\=\; & [ id + \sigma , i_2 \circ [ \tau , {[ later \circ now , later \circ f]}^* \circ now \circ i_2 ] ] \circ w\tag*{(\ref{eq:later*})}
-    =\; & [ id + \sigma , i_2 \circ [ \tau , later \circ f ] ] \circ w
+    \\=\; & [ id + \sigma , i_2 \circ [ \tau , later \circ f ] ] \circ w
   \end{alignat*}
 
-  \todo[inline]{The second to last step uses that $f^* \circ later = (later \circ f)^*$ this should be proven somewhere and referenced here.}
-  \todo[inline]{The fact that $f^* \circ Dg = (f \circ g)^*$ should be mentioned somewhere (in preliminaries!)}
-
-  \change[inline]{Move this remark to the beginning of proof}
-  The first step in both equations can be proven by monicity of $out$ and then using \ref{D3} and the dual diagram for $\sigma$ which is a direct consequence of \ref{D3}:
-  % https://q.uiver.app/#q=WzAsNSxbMCwwLCJYIFxcdGltZXMgRFkiXSxbMCwxLCJEKFggXFx0aW1lcyBZKSJdLFs0LDAsIlggXFx0aW1lcyBZICsgWCBcXHRpbWVzIERZIl0sWzQsMSwiWCBcXHRpbWVzIFkgK0QoWCBcXHRpbWVzIFkpIl0sWzIsMCwiWCBcXHRpbWVzIChZICsgRFkpIl0sWzAsMSwiXFxzaWdtYSJdLFsxLDMsIm91dCJdLFsyLDMsImlkICsgXFxoYXR7XFx0YXV9IiwyXSxbMCw0LCJpZCBcXHRpbWVzIG91dCJdLFs0LDIsImRzdGwiXV0=
-  \[\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["\sigma", from=1-1, to=2-1]
-      \arrow["out", from=2-1, to=2-5]
-      \arrow["{id + \hat{\tau}}"', from=1-5, to=2-5]
-      \arrow["{id \times out}", from=1-1, to=1-3]
-      \arrow["dstl", from=1-3, to=1-5]
-    \end{tikzcd}\]
-
   Let us now check the first step in the equation for $\sigma^* \circ \tau$, the same step for $\tau^* \circ \sigma$ is then symmetric.
 
   Again we proceed by monicity of $out$:
@@ -467,18 +516,18 @@ Let us record some facts that we will use to prove commutativity of $\mathbf{D}$
      & out \circ \sigma^* \circ \tau
     \\=\;&[ out \circ \sigma , i_2 \circ \sigma^* ] \circ out \circ \tau\tag*{\ref{D2}}
     \\=\;&[ out \circ \sigma , i_2 \circ \sigma^* ] \circ (id + \tau) \circ dstl \circ (id \times out)\tag*{\ref{D3}}
-    \\=\;&[ (id + \sigma) \circ dstr \circ (out \times id) , i_2 \circ \sigma^* \circ \tau ] \circ dstl \circ (id \times out)\tag*{(outsigma)}
+    \\=\;&[ (id + \sigma) \circ dstr \circ (out \times id) , i_2 \circ \sigma^* \circ \tau ] \circ dstl \circ (id \times out)\tag*{\ref{sigma1}}
     \\=\;&[ (id + \sigma) \circ dstr \circ (out \times id) , i_2 \circ \sigma^* \circ \tau ] \circ ((out^{-1} \times id) + (out^{-1} \times id)) \circ dstl \circ (out \times out)
     \\=\;&[ (id + \sigma) \circ dstr, i_2 \circ \sigma^* \circ \tau \circ (out^{-1} \times id)] \circ dstl \circ (out \times out)
     \\=\;&[ (id + \sigma) \circ dstr, i_2 \circ \sigma^* \circ D(out^{-1} \times id) \circ \tau] \circ dstl \circ (out \times out)
     \\=\;&[ (id + \sigma) \circ dstr, i_2 \circ (\sigma \times (out^{-1} \times id))^* \circ \tau] \circ dstl \circ (out \times out)
-    \\=\;&[ (id + \sigma) \circ dstr, i_2 \circ (out^{-1} \circ (id + \sigma) \circ dstr)^* \circ \tau] \circ dstl \circ (out \times out)\tag*{($\sigma$)}
+    \\=\;&[ (id + \sigma) \circ dstr, i_2 \circ (out^{-1} \circ (id + \sigma) \circ dstr)^* \circ \tau] \circ dstl \circ (out \times out)\tag*{\ref{sigma2}}
     \\=\;&[ (id + \sigma) \circ dstr, i_2 \circ (out^{-1} \circ (id + \sigma))^* \circ Ddstr \circ \tau] \circ dstl \circ (out \times out)
     \\=\;&[ (id + \sigma) \circ dstr, i_2 \circ (out^{-1} \circ (id + \sigma))^* \circ [D i_1 \circ \tau , D i_2 \circ \tau] \circ dstr] \circ dstl \circ (out \times out)\tag*{\ref{Dcomm-helper}}
     \\=\;&[ (id + \sigma), i_2 \circ (out^{-1} \circ (id + \sigma))^* \circ [D i_1 \circ \tau , D i_2 \circ \tau]] \circ (dstr + dstr) \circ dstl \circ (out \times out)
     \\=\;&[ (id + \sigma), i_2 \circ [(out^{-1} \circ i_1)^* \circ \tau , (out^{-1} \circ i_2 \circ \sigma)^* \circ \tau]] \circ w
     \\=\;&[ (id + \sigma), i_2 \circ [ \tau , (later \circ \sigma)^* \circ \tau]] \circ w \tag*{\ref{K1}}
-    \\=\;&[ (id + \sigma), i_2 \circ [ \tau , later \circ \sigma^* \circ \tau]] \circ w \tag*{(later)}
+    \\=\;&[ (id + \sigma), i_2 \circ [ \tau , later \circ \sigma^* \circ \tau]] \circ w \tag*{(\ref{eq:later*})}
   \end{alignat*}
 
   where
@@ -491,8 +540,6 @@ Let us record some facts that we will use to prove commutativity of $\mathbf{D}$
     \\=\;&[ Ddstr \circ D(i_1 \times id) \circ \tau , Ddstr \circ D(i_2 \times id) \circ \tau ]
     \\=\;&[ Di_1 \circ \tau , Di_2 \circ \tau ]
   \end{alignat*}
-  \todo[inline]{Add $dstl-i_1$ etc. to preliminaries as corollary!}
-
 \end{proof}
 
 \improvement[inline]{Elaborate more?}