Work on thesis

.gitignore

@@ -57,3 +57,4 @@ thesis/main.bcf-SAVE-ERROR
 thesis/main.tdo
 main.synctex(busy)
 thesis/main.pyg
+thesis/main.loe

thesis/.vscode/ltex.hiddenFalsePositives.en-GB.txt

@@ -1,2 +1,4 @@
 {"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\Q[agda] linenos=true, breaklines=true, encoding=utf8, fontsize=, frame=lines, autogobble\\E$"}
 {"rule":"WHITESPACE_RULE","sentence":"^\\Q[4][]##4\\E$"}
+{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\Q[ignoreall,show=definition]\\E$"}
+{"rule":"COMMA_PARENTHESIS_WHITESPACE","sentence":"^\\Q[ignoreall,show=definition]\\E$"}

thesis/.vscode/ltex.hiddenFalsePositives.en-US.txt

@@ -19,3 +19,4 @@
 {"rule":"ENGLISH_WORD_REPEAT_RULE","sentence":"^\\QA (unguarded) Elgot Algebra \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q consists of: An object X for every \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q the iteration \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, satisfying: law:fixpoint Fixpoint: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q Uniformity: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q Folding: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q test: \\E(?:Dummy|Ina|Jimmy-)[0-9]+$"}
 {"rule":"ENGLISH_WORD_REPEAT_RULE","sentence":"^\\QA (unguarded) Elgot Algebra \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q consists of: An object X for every \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q the iteration \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, satisfying: law:fixpoint Fixpoint: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q law:uniformity Uniformity: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q law:folding Folding: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q test: \\E(?:Dummy|Ina|Jimmy-)[0-9]+$"}
 {"rule":"ENGLISH_WORD_REPEAT_RULE","sentence":"^\\QA (unguarded) Elgot Algebra \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q consists of: An object X for every \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q the iteration \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, satisfying: law:fixpoint Fixpoint: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q law:uniformity Uniformity: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q law:folding Folding: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for \\E(?:Dummy|Ina|Jimmy-)[0-9]+$"}
+{"rule":"ENGLISH_WORD_REPEAT_RULE","sentence":"^\\Qlaw:diamond Diamond\\E$"}

thesis/main.tex

@@ -16,6 +16,7 @@
 \usepackage{amssymb}
 \usepackage{amsthm}
 \usepackage{thmtools}
+\usepackage{thmtools}
 \usepackage{fancyvrb}
 \usepackage{mathtools}
 \usepackage{amsmath}
@@ -24,6 +25,7 @@
 % packages for draft version
 \usepackage{lineno}
 \usepackage[colorinlistoftodos,prependcaption,textsize=tiny,obeyDraft]{todonotes}
+\usepackage{ifdraft}
 
 % mathpartir uses \atop, amsmath overrides it to throw a warning tho, so we override it back to the original!
 \makeatletter
@@ -191,7 +193,7 @@ Erlangen, \today{} \rule{7cm}{1pt}\\
 }
 \makeatother
 
-\linenumbers
+\ifdraft{\linenumbers}
 
 % \include{src/examples}
 \include{src/00_introduction}
@@ -204,6 +206,7 @@ Erlangen, \today{} \rule{7cm}{1pt}\\
 
 \todo[inline]{Symbolverzeichnis, siehe: https://www.namsu.de/Extra/pakete/Listofsymbols.pdf}
 \todo[inline]{Add fullstop behind every proof}
+\todo[inline]{ (Re-) move list of definitions}
 
 \appendix
 % \include{src/A1_contributions}
@@ -211,6 +214,10 @@ Erlangen, \today{} \rule{7cm}{1pt}\\
 \medskip
 
 \printbibliography[heading=bibintoc]{}
+
+% https://tex.stackexchange.com/questions/74857/toc-like-list-of-definitions-using-theorem-environments
+\renewcommand*{\listtheoremname}{List of Definitions}
+\listoftheorems[ignoreall,show={definition}]
 \end{document}
 
 % vim: tw=80 nospell spelllang=en nocul

thesis/src/04_iteration.tex

@@ -21,6 +21,9 @@ In this chapter we will draw on the inherent connection between partiality and i
   \end{itemize}
 \end{definition}
 
+\todo[inline]{Diamond and stutter laws}
+\customlabel{law:diamond}{\textbf{Diamond}}
+
 Morphisms between Elgot algebras that are coherent with respect to the iteration operator are of special interest to us, the following definition classifies them.
 
 \begin{definition}
@@ -566,7 +569,7 @@ As we did when proving commutativity of $\mathbf{D}$, let us record some facts a
   $\sigma$ is left iteration preserving and satisfies $\sigma \circ (\eta \times id) = \eta$ and the following properties of $\tau$ and $\sigma$ hold.
   \begin{alignat*}{2}
     &\tau \circ (f^* \times g^*) &&= (\tau \circ (id \times g))^* \circ \tau \circ (f^* \times id)\tag{$\tau_1$}\label{Ktau1}
-    \\&\sigma \circ (f^* \times g^*) &&= (\sigma \circ (f \times id))^* \circ \tau \circ (id \times g^*)\tag{$\sigma_1$}\label{Ksigma1}
+    \\&\sigma \circ (f^* \times g^*) &&= (\sigma \circ (f \times id))^* \circ \sigma \circ (id \times g^*)\tag{$\sigma_1$}\label{Ksigma1}
   \end{alignat*}
 \end{corollary}
 \begin{proof}
@@ -593,10 +596,121 @@ As we did when proving commutativity of $\mathbf{D}$, let us record some facts a
   \begin{itemize}
     \item[(\ref{Ktau1})] 
     \begin{alignat*}{1}
-      todo
+      &(\tau \circ (id \times g))^* \circ \tau \circ (f^* \times id)
+      \\=\;&\tau^* \circ K(id \times g) \circ \tau \circ (f^* \times id)
+      \\=\;&\tau^* \circ \tau \circ (id \times Kg) \circ (f^* \times id)
+      \\=\;&\tau \circ (id \times \mu) \circ (id \times Kg) \circ (f^* \times id)
+      \\=\;&\tau \circ (id \times g^*) \circ (f^* \times id)
+      \\=\;&\tau \circ (f^* \times g^*)
+    \end{alignat*}
+
+    \item[(\ref{Ksigma1})]
+    \begin{alignat*}{1}
+      &(\sigma \circ (f \times id))^* \circ \sigma \circ (id \times g^*)
+      \\=\;&\sigma^* \circ K(f \times id) \circ \sigma \circ (id \times g^*)
+      \\=\;&\sigma^* \circ \sigma \circ (Kf \times id) \circ (id \times g^*)
+      \\=\;&\sigma \circ (\mu \times id) \circ (Kf \times id) \circ (id \times g^*)
+      \\=\;&\sigma \circ (f^* \times id) \circ (id \times g^*)
+      \\=\;&\sigma \circ (f^* \times g^*)
     \end{alignat*}
   \end{itemize}
+\end{proof}
 
+The following Lemma is central to the proof of commutativity.
+
+\begin{lemma}\label{lem:KCommKey} Given $f : X \rightarrow KY + Z, g : Z \rightarrow KA + Z$,
+  \[\tau^* \circ \sigma \circ (((\eta + id) \circ f)^\# \times ((\eta + id) \circ g)^\#) = \sigma^* \circ \tau \circ (((\eta + id) \circ f)^\# \times ((\eta + id) \circ g)^\#).\]
+\end{lemma}
+\begin{proof}
+  Let us abbreviate $\hat{f} := (\eta + id) \circ f$ and $\hat{g} := (\eta + id) \circ g$. It suffices to find a $w : ?$ such that $\hat{f}^\# \circ \pi_1 = [ \hat{f}^\# \circ \pi_1 , \eta \circ \pi_1 ]^* \circ w^\#$ and $\hat{g}^\# \circ \pi_2 = [ \hat{g}^\# \circ \pi_2 , \eta \circ \pi_2 ]^* \circ w^\#$, then
+  \begin{alignat*}{1}
+    &\tau^* \circ \sigma \circ (\hat{f}^\# \times \hat{g}^\#)
+    \\=\;&\tau^* \circ \sigma \circ ([ \hat{f}^\# \circ \pi_1 , \eta \circ \pi_1 ]^* \times [ \hat{g}^\# \circ \pi_2 , \eta \circ \pi_2 ]^*) \circ (w^\# \times w^\#)
+    \\=\;&\tau^* \circ (\sigma \circ ([ \hat{f}^\# \circ \pi_1 , \eta \circ \pi_1 ] \times id))^* \circ \sigma \circ (id \times [ \hat{g}^\# \circ \pi_2 , \eta \circ \pi_2 ]^*) \circ (w^\# \times w^\#)
+    \\=\;&\tau^* \circ (\sigma \circ ([ \hat{f}^\# \circ \pi_1 , \eta \circ \pi_1 ] \times id))^* \circ K(id \times [ \hat{g}^\# \circ \pi_2 , \eta \circ \pi_2 ]^*) \circ \sigma \circ (w^\# \times w^\#)
+    \\=\;&\tau^* \circ (\sigma \circ ([ \hat{f}^\# \circ \pi_1 , \eta \circ \pi_1 ] \times id))^* \circ K(id \times [ \hat{g}^\# \circ \pi_2 , \eta \circ \pi_2 ]^*) \circ Kswap \circ \tau \circ \Delta \circ w^\#
+    \\=\;&\tau^* \circ (\sigma \circ ([ \hat{f}^\# \circ \pi_1 , \eta \circ \pi_1 ] \times id))^* \circ K(id \times [ \hat{g}^\# \circ \pi_2 , \eta \circ \pi_2 ]^*) \circ Kswap \circ K\langle \eta , id \rangle \circ w^\#\tag{\ref{thm:Klifting}}
+    \\=\;&\tau^* \circ (\sigma \circ ([ \hat{f}^\# \circ \pi_1 , \eta \circ \pi_1 ] \times id))^* \circ K(id \times [ \hat{g}^\# \circ \pi_2 , \eta \circ \pi_2 ]^*) \circ K\langle id , \eta \rangle \circ w^\#
+    \\=\;&\tau^* \circ (\sigma \circ ([ \hat{f}^\# \circ \pi_1 , \eta \circ \pi_1 ] \times id))^* \circ K\langle id , [ \hat{g}^\# \circ \pi_2 , \eta \circ \pi_2 ]\rangle \circ w^\#
+    \\=\;&\tau^* \circ (\sigma \circ \langle[ \hat{f}^\# \circ \pi_1 , \eta \circ \pi_1 ] , [ \hat{g}^\# \circ \pi_2 , \eta \circ \pi_2 ]\rangle)^* \circ w^\#
+    \\=\;&\tau^* \circ (\sigma \circ [\langle \hat{f}^\# \circ \pi_1 , \eta \circ \pi_2 \rangle , \langle \eta \circ \pi_1 , \hat{g}^\# \circ \pi_2 \rangle])^* \circ w^\#
+    \\=\;&(\tau^* \circ \sigma \circ [\hat{f}^\# \times \eta , \eta \times \hat{g}^\#])^* \circ w^\#
+    \\=\;&([\tau^* \circ \sigma \circ (\hat{f}^\# \times \eta) , \tau^* \circ \sigma \circ (\eta \times \hat{g}^\#)])^* \circ w^\#
+    \\=\;&([\tau^* \circ K(id \times \eta) \circ \sigma \circ (\hat{f}^\# \times id) , \tau^* \circ \eta \circ (id \times \hat{g}^\#)])^* \circ w^\#
+    \\=\;&([\sigma \circ (\hat{f}^\# \times id) , \tau \circ (id \times \hat{g}^\#)])^* \circ w^\#,
+  \end{alignat*}
+
+  \todo[inline]{Full proofs or 'symmetric' enough?}
+  and by a symmetric argument also
+  \[\sigma^* \circ \tau \circ (\hat{f}^\# \times \hat{g}^\#) = ([\sigma \circ (\hat{f}^\# \times id) , \tau \circ (id \times \hat{g}^\#)])^* \circ w^\#.\]
+  % \begin{alignat*}{1}
+  %   &\sigma^* \circ \tau \circ (\hat{f}^\# \times \hat{g}^\#)
+  %   \\=\;&\sigma^* \circ \tau \circ ([ \hat{f}^\# \circ \pi_1 , \eta \circ \pi_1 ]^* \times [ \hat{g}^\# \circ \pi_2 , \eta \circ \pi_2 ]^*) \circ (w^\# \times w^\#)
+  %   \\=\;&\sigma^* \circ (\tau \circ (id \times [ \hat{g}^\# \circ \pi_2 , \eta \circ \pi_2 ]))^* \circ \tau \circ ([ \hat{f}^\# \circ \pi_1 , \eta \circ \pi_1 ]^* \times id) \circ (w^\# \times w^\#)
+  %   \\=\;&\sigma^* \circ (\tau \circ (id \times [ \hat{g}^\# \circ \pi_2 , \eta \circ \pi_2 ]))^* \circ K([ \hat{f}^\# \circ \pi_1 , \eta \circ \pi_1 ]^* \times id) \circ \tau \circ (w^\# \times w^\#)
+  %   \\=\;&\sigma^* \circ (\tau \circ (id \times [ \hat{g}^\# \circ \pi_2 , \eta \circ \pi_2 ]))^* \circ K([ \hat{f}^\# \circ \pi_1 , \eta \circ \pi_1 ]^* \times id) \circ \tau \circ \Delta \circ w^\#\tag{\ref{thm:Klifting}}
+  %   \\=\;&\sigma^* \circ (\tau \circ (id \times [ \hat{g}^\# \circ \pi_2 , \eta \circ \pi_2 ]))^* \circ K([ \hat{f}^\# \circ \pi_1 , \eta \circ \pi_1 ]^* \times id) \circ K\langle \eta , id \rangle \circ w^\#
+  %   \\=\;&\sigma^* \circ (\tau \circ (id \times [ \hat{g}^\# \circ \pi_2 , \eta \circ \pi_2 ]))^* \circ K\langle[ \hat{f}^\# \circ \pi_1 , \eta \circ \pi_1 ] , id\rangle \circ w^\#
+  %   \\=\;&\sigma^* \circ (\tau \circ \langle [ \hat{f}^\# \circ \pi_1 , \eta \circ \pi_1 ] , [ \hat{g}^\# \circ \pi_2 , \eta \circ \pi_2 ]\rangle)^* \circ w^\#
+  %   \\=\;&\sigma^* \circ (\tau \circ \langle [ \hat{f}^\# \circ \pi_1 , \eta \circ \pi_1 ] , [ \hat{g}^\# \circ \pi_2 , \eta \circ \pi_2 ]\rangle)^* \circ w^\#
+  %   \\=\;&\sigma^* \circ (\tau \circ [ \hat{f}^\# \times \eta , \eta \times \hat{g}^\# ])^* \circ w^\#
+  %   \\=\;&([ \sigma^* \circ \tau \circ (\hat{f}^\# \times \eta) , \sigma^* \circ \tau \circ (\eta \times \hat{g}^\#) ])^* \circ w^\#
+  %   \\=\;&([ \sigma^* \circ \eta \circ (\hat{f}^\# \times id) , \sigma^* \circ K(\eta \times id) \circ \tau \circ (id \times \hat{g}^\#) ])^* \circ w^\#
+  %   \\=\;&([ \sigma \circ (\hat{f}^\# \times id) , \tau \circ (id \times \hat{g}^\#) ])^* \circ w^\#.
+  % \end{alignat*}
+
+  Note that we are referencing \autoref{thm:Klifting} even though for a monad to be an equational lifting monad it has to be commutative first. However, we are merely referencing the equational law, which can (and does in this case) hold without depending on commutativity.
+
+  We are thus left to find such a $w$, consider
+  \[w := [ i_1 \circ K i_1 \circ \tau , ((K i_2 \circ \sigma) + id) \circ dstr \circ (\hat{f} \times id) ] \circ dstl \circ (id \times \hat{g}). \]
+  $w$ indeed satisfies the requisite properties, let us check the first property, the second one follows by a symmetric argument. We will show that
+  \[[ \hat{f}^\# \circ \pi_1 , \eta \circ \pi_1 ]^* \circ w^\# = ([ i_1 \circ \pi_1 , (\hat{f}^\# \circ \pi_1 + id) \circ dstl ] \circ dstr \circ (\hat{f} \times g))^\# = \hat{f}^\# \circ \pi_1. \]
+  Indeed,
+  \begin{alignat*}{1}
+    &[ \hat{f}^\# \circ \pi_1 , \eta \circ \pi_1 ]^* \circ w^\#
+    \\=\;&(([ \hat{f}^\# \circ \pi_1 , \eta \circ \pi_1 ]^* + id) \circ w)^\#
+    \\=\;&([ i_1 \circ (\hat{f}^\# \circ \pi_1)^* \circ \tau , ((K\pi_1 \circ \sigma) + id) \circ dstr \circ (\hat{f} \times id) ] \circ dstl \circ (id \times \hat{g}))^\#
+    \\=\;&([ i_1 \circ (\hat{f}^\# \circ \pi_1)^* \circ \tau , ((K\pi_1 \circ \sigma) + id) \circ dstr \circ (\hat{f} \times id) ] \circ dstl \circ (id \times (\eta + id)) \circ (id \times g))^\#
+    \\=\;&([ i_1 \circ (\hat{f}^\# \circ \pi_1)^* \circ \tau , ((K\pi_1 \circ \sigma) + id) \circ dstr \circ (\hat{f} \times id) ] \circ ((id \times \eta) + id) \circ dstl \circ (id \times g))^\#
+    \\=\;&([ i_1 \circ (\hat{f}^\# \circ \pi_1)^* \circ \tau \circ (id \times \eta) , ((K\pi_1 \circ \sigma) + id) \circ dstr \circ (\hat{f} \times id) ] \circ dstl \circ (id \times g))^\#
+    \\=\;&([ i_1 \circ \hat{f}^\# \circ \pi_1 , ((K\pi_1 \circ \sigma) + id) \circ dstr \circ (\hat{f} \times id) ] \circ dstl \circ (id \times g))^\#
+    \\=\;&([ i_1 \circ [id , \hat{f}^\#] \circ \hat{f} \circ \pi_1 , ((K\pi_1 \circ \sigma) + id) \circ dstr \circ (\hat{f} \times id) ] \circ dstl \circ (id \times g))^\#\tag{\ref{law:fixpoint}}
+    \\=\;&([ i_1 \circ [id , \hat{f}^\#] \circ \pi_1 \circ (\hat{f} \times id) , ((K\pi_1 \circ \sigma) + id) \circ dstr \circ (\hat{f} \times id) ] \circ dstl \circ (id \times g))^\#
+    \\=\;&([ i_1 \circ [id , \hat{f}^\#] \circ \pi_1 , ((K\pi_1 \circ \sigma) + id) \circ dstr ] \circ ((\hat{f} \times id) + (\hat{f} \times id)) \circ dstl \circ (id \times g))^\#
+    \\=\;&([ i_1 \circ [id , \hat{f}^\#] \circ \pi_1 , ((K\pi_1 \circ \sigma) + id) \circ dstr ] \circ dstl \circ (\hat{f} \times g))^\#
+    \\=\;&([ i_1 \circ [id , \hat{f}^\#] \circ (\pi_1 + \pi_1) \circ dstr , ((K\pi_1 \circ \sigma) + id) \circ dstr ] \circ dstl \circ (\hat{f} \times g))^\#
+    \\=\;&([ i_1 \circ [id , \hat{f}^\#] \circ (\pi_1 + \pi_1) , ((K\pi_1 \circ \sigma) + id) ] \circ (dstr + dstr) \circ dstl \circ (\hat{f} \times g))^\#
+    \\=\;&([ i_1 \circ [id , \hat{f}^\#] \circ (\pi_1 + \pi_1) , ((K\pi_1 \circ \sigma) + id) ] \circ [ i_1 + i_1 , i_2 + i_2 ] \circ (dstl + dstl) \circ dstr \circ (\hat{f} \times g))^\#
+    \\=\;&([ [ i_1 \circ [id , \hat{f}^\#] \circ i_1 \circ \pi_1 , i_1 \circ K\pi_1 \circ \sigma ] , [ i_1 \circ [id , \hat{f}^\#] \circ i_2 \circ \pi_1 , i_2 ] ] \circ (dstl + dstl) \circ dstr \circ (\hat{f} \times g))^\#
+    \\=\;&([ [ i_1 \circ \pi_1 , i_1 \circ \pi_1 ] , [ i_1 \circ \hat{f}^\# \circ \pi_1 , i_2 ] ] \circ (dstl + dstl) \circ dstr \circ (\hat{f} \times g))^\#
+    \\=\;&([ i_1 \circ [ \pi_1 , \pi_1 ] , (\hat{f}^\# \circ \pi_1 + id) ] \circ (dstl + dstl) \circ dstr \circ (\hat{f} \times g))^\#
+    \\=\;&([ i_1 \circ \pi_1 , (\hat{f}^\# \circ \pi_1 + id) \circ dstl ] \circ dstr \circ (\hat{f} \times g))^\#
+  \end{alignat*}
+  and
+  \begin{alignat*}{1}
+    &\hat{f}^\# \circ \pi_1
+    \\=\;&((id + \Delta) \circ h)^\# \tag{\ref{law:uniformity}}
+    \\=\;&([ i_1 , ((id + \Delta) \circ h)^\# + id] \circ h)^\# \tag{\ref{law:diamond}}
+    \\=\;&([ i_1 , (\hat{f}^\# \circ \pi_1) + id ] \circ h)^\# \tag{\ref{law:uniformity}}
+    \\=\;&([ i_1 \circ \pi_1 , ((\hat{f} \circ \pi_1 \circ \pi_1) + (\pi_1 \times id)) \circ dstl \circ \langle id , g \circ \pi_2 \rangle ] \circ dstr \circ (\hat{f} \times id))^\#
+    \\=\;&([ i_1 \circ \pi_1 , ((\hat{f} \circ \pi_1) + id) \circ ((\pi_1 \times id) + (\pi_1 \times id)) \circ dstl \circ \langle id , g \circ \pi_2 \rangle ] \circ dstr \circ (\hat{f} \times id))^\#
+    \\=\;&([ i_1 \circ \pi_1 , ((\hat{f} \circ \pi_1) + id) \circ dstl \circ \langle \pi_1 , g \circ \pi_2 \rangle ] \circ dstr \circ (\hat{f} \times id))^\#
+    \\=\;&([ i_1 \circ \pi_1 \circ (id \times g) , ((\hat{f} \circ \pi_1) + id) \circ dstl \circ (id \times g) ] \circ dstr \circ (\hat{f} \times id))^\#
+    \\=\;&([ i_1 \circ \pi_1 , ((\hat{f} \circ \pi_1) + id) \circ dstl ] \circ dstr \circ (\hat{f} \times g))^\#,
+  \end{alignat*}
+
+  where $h = (\pi_1 + ((\pi_1 + (\pi_1 \times id)) \circ dstl \circ \langle id , g \circ \pi_2 \rangle)) \circ dstr \circ (\hat{f} \times id)$ and the application of \ref{law:uniformity} is justified, since
+  \begin{alignat*}{1}
+    &(id + \pi_1) \circ (id + \Delta) \circ h
+    \\=\;&(\pi_1 + ((\pi_1 \circ [ \pi_1 , \pi_1 \times id ]) \circ dstl \circ \langle id , g \circ \pi_2 \rangle)) \circ dstr \circ (\hat{f} \times id)
+    \\=\;&(\pi_1 + ([ \pi_1 \circ \pi_1 , \pi_1 \circ \pi_1 ] \circ dstl \circ \langle id , g \circ \pi_2 \rangle)) \circ dstr \circ (\hat{f} \times id)
+    \\=\;&(\pi_1 + (\pi_1 \circ \pi_1 \circ \langle id , g \circ \pi_2 \rangle)) \circ dstr \circ (\hat{f} \times id)
+    \\=\;&(\pi_1 + \pi_1) \circ dstr \circ (\hat{f} \times id)
+    \\=\;&\pi_1 \circ (\hat{f} \times id)
+    \\=\;&\hat{f} \circ \pi_1
+  \end{alignat*}
+
+  This concludes the proof.
 \end{proof}
 
 \begin{theorem}
@@ -638,7 +752,7 @@ As we did when proving commutativity of $\mathbf{D}$, let us record some facts a
 \todo[inline]{Introduce Diamond and Stutter laws}
 \end{proof}
 
-\begin{theorem}
+\begin{theorem}\label{thm:Klifting}
   $\mathbf{K}$ is an equational lifting monad.
 \end{theorem}