leonv/bsc-leon-vatthauer
1
0
Fork 0
mirror of https://git8.cs.fau.de/theses/bsc-leon-vatthauer.git synced 2024-05-31 07:28:34 +02:00
Code Issues Projects Releases Packages Wiki Activity

Improve proof of strength for K

Browse source
This commit is contained in:
Leon Vatthauer 2024-03-07 11:00:04 +01:00
parent 69696cb76d
commit 39d83c6dfe
Signed by: leonv
SSH key fingerprint: SHA256:G4+ddwoZmhLPRB1agvXzZMXIzkVJ36dUYZXf5NxT+u8
3 changed files with 147 additions and 47 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
thesis/main.tex
View file

@ -1,4 +1,4 @@
\documentclass[a4paper,11pt,numbers=noenddot]{scrbook}
\documentclass[a4paper,11pt,numbers=noenddot,draft]{scrbook}
\usepackage[top=2cm,lmargin=1in,rmargin=1in,bottom=3cm,hmarginratio=1:1]{geometry}
\usepackage[ngerman, main=british]{babel}
@ -21,6 +21,10 @@
\usepackage{amsmath}
\usepackage{mathabx}
\usepackage{mathpartir}
% packages for draft version
\usepackage{lineno}
\usepackage[colorinlistoftodos,prependcaption,textsize=tiny,obeyDraft]{todonotes}
% mathpartir uses \atop, amsmath overrides it to throw a warning tho, so we override it back to the original!
\makeatletter
\let\atop\@@atop
@ -104,7 +108,6 @@
% \setmathfont{STIX Two Math Regular}
\usepackage{mathrsfs}
\usepackage[colorinlistoftodos,prependcaption,textsize=tiny]{todonotes}
\usepackage{xargs}
\usepackage{xstring}
@ -188,6 +191,7 @@ Erlangen, \today{} \rule{7cm}{1pt}\\
}
\makeatother
\linenumbers
% \include{src/examples}
\include{src/00_introduction}

9
thesis/src/01_preliminaries.tex
View file

@ -192,6 +192,8 @@ Let $F : \C \rightarrow \C$ be an endofunctor. Recall that F-algebras are tuples
\end{definition}
\todo[inline]{Adopt text, lemma style}
\begin{proposition}
F-coalgebras together with their morphisms form a category that we call $Coalg(F)$.
\end{proposition}
@ -414,9 +416,10 @@ As with monads we can now consider the category of strong monads:
Now we can express the above condition:
\begin{definition}[Commutative Monad]
A strong monad $\mathbf{T}$ is called commutative if the (right) strength $\tau$ commutes with the induced (left) strength:
\[\sigma_{X,Y} = Mswap \circ \tau_{Y,X} \circ swap : TX \times Y \rightarrow T(X \times Y)\]
Concretely, $\mathbf{T}$ is called strong if the following diagram commutes:
A strong monad $\mathbf{T}$ is called commutative if the (right) strength $\tau$ commutes with the induced left strength
\[\sigma_{X,Y} = Tswap \circ \tau_{Y,X} \circ swap : TX \times Y \rightarrow T(X \times Y)\]
that satisfies symmetrical conditions to the ones $\tau$ satisfies.
Concretely, $\mathbf{T}$ is called commutative if the following diagram commutes:
% https://q.uiver.app/#q=WzAsNCxbMCwyLCJUKFggXFx0aW1lcyBUWSkiXSxbMiwwLCJUKFRYIFxcdGltZXMgWSkiXSxbMiwyLCJUKFggXFx0aW1lcyBZKSJdLFswLDAsIlRYIFxcdGltZXMgVFkiXSxbMywxLCJcXHRhdSJdLFszLDAsIlxcc2lnbWEiLDJdLFswLDIsIlxcdGF1XioiLDJdLFsxLDIsIlxcc2lnbWFeKiJdXQ==
\[\begin{tikzcd}
{TX \times TY} && {T(TX \times Y)} \\

177
thesis/src/04_iteration.tex
View file

@ -1,4 +1,4 @@
\chapter{Iteration Algebras and Monads}\label{chp:iteration}
\chapter{Iteration Algebras and Monads}~\label{chp:iteration}
In this chapter we will draw on the inherent connection between partiality and iteration to establish a partiality monad in a general setting without axioms by utilizing previous research on iteration theories.
\section{Elgot Algebras}
@ -199,12 +199,12 @@ Products and exponentials of Elgot algebras can be formed in a canonical way.
\\=\;&curry(((eval + id) \circ dstr \circ ([ (id + i_1) \circ f , i_2 \circ h ] \times id))^{\#_a})\tag{\ref{law:uniformity}}
\\=\;&[ (id + i_1) \circ f , i_2 \circ h ]^\#
\end{alignat*}
Where the first application of \ref{law:uniformity} is justified by:
\begin{alignat*}{1}
&(id + dstr) \circ (((eval + id) \circ dstr \circ (f \times id))^{\#_a} + (h \times id)) \circ dstr
\\=\;&(((eval + id) \circ dstr \circ (f \times id))^{\#_a} + (dstr \circ (h \times id))) \circ dstr
\end{alignat*}
which follows instantly, and the second application is justified by:
% Where the first application of \ref{law:uniformity} is justified by:
% \begin{alignat*}{1}
% &(id + dstr) \circ (((eval + id) \circ dstr \circ (f \times id))^{\#_a} + (h \times id)) \circ dstr
% \\=\;&(((eval + id) \circ dstr \circ (f \times id))^{\#_a} + (dstr \circ (h \times id))) \circ dstr
% \end{alignat*}
The second application of \ref{law:uniformity} is non-trivial, using epicness of $dstr^{-1}$:
\begin{alignat*}{1}
&(id + dstr) \circ (eval + id) \circ dstr \circ ([ (id + i_1) \circ f , i_2 \circ h ] \times id) \circ dstr^{-1}
\\=\;&[ (id + dstr) \circ (eval + id) \circ dstr \circ ([ (id + i_1) \circ f , i_2 \circ h ] \times id) \circ (i_1 \times id)
@ -216,9 +216,8 @@ Products and exponentials of Elgot algebras can be formed in a canonical way.
\\=\;&[ (id + dstr) \circ (eval + id) \circ (id + (i_1 \times id)) \circ dstr \circ (f \times id)
\\&, (id + dstr) \circ (eval + id) \circ i_2 \circ (h \times id) ]
\\=\;&[ (eval + i_1) \circ dstr \circ (f \times id) , i_2 \circ dstr \circ (h \times id) ]
\\=\;&[ (id + i_1) \circ (eval + id) \circ dstr \circ (f \times id) , i_2 \circ dstr \circ (h \times id) ] \circ dstr \circ dstr^{-1}
\\=\;&[ (id + i_1) \circ (eval + id) \circ dstr \circ (f \times id) , i_2 \circ dstr \circ (h \times id) ] \circ dstr \circ dstr^{-1}.
\end{alignat*}
which uses epicness of $dstr^{-1}$.
\end{itemize}
\end{proof}
@ -309,14 +308,14 @@ A symmetrical variant of the previous definition is sometimes useful.
\end{alignat*}
for any $Z \in \obj{\C}, h : Z \rightarrow KY + Z$.
Where the application of \ref{law:uniformity} is justified by
\begin{alignat*}{1}
&(id + swap) \circ ((\ls{f \circ swap} \circ swap) + id) \circ dstl \circ (id \times h)
\\=\;&((\ls{f \circ swap} \circ swap) + swap) \circ dstl \circ (id \times h)
\\=\;&(\ls{f \circ swap} + id) \circ (swap + swap) \circ dstl \circ (id \times h)
\\=\;&(\ls{f \circ swap} + id) \circ dstr \circ swap \circ (id \times h)
\\=\;&(\ls{f \circ swap} + id) \circ dstr \circ (h \times id) \circ swap.
\end{alignat*}
% Where the application of \ref{law:uniformity} is justified by
% \begin{alignat*}{1}
% &(id + swap) \circ ((\ls{f \circ swap} \circ swap) + id) \circ dstl \circ (id \times h)
% \\=\;&((\ls{f \circ swap} \circ swap) + swap) \circ dstl \circ (id \times h)
% \\=\;&(\ls{f \circ swap} + id) \circ (swap + swap) \circ dstl \circ (id \times h)
% \\=\;&(\ls{f \circ swap} + id) \circ dstr \circ swap \circ (id \times h)
% \\=\;&(\ls{f \circ swap} + id) \circ dstr \circ (h \times id) \circ swap.
% \end{alignat*}
The requisite diagram commutes, since
\begin{alignat*}{1}
@ -344,13 +343,13 @@ A symmetrical variant of the previous definition is sometimes useful.
\end{alignat*}
for any $Z \in \obj{\C}, h : Z \rightarrow KY + Z$.
The application of \ref{law:uniformity} is justified by
\begin{alignat*}{1}
&(id + swap) \circ ((g \circ swap) + id) \circ dstr \circ (h \times id)
\\=\;&(g + id) \circ (swap + swap) \circ dstr \circ (h \times id)
\\=\;&(g + id) \circ dstl \circ swap \circ (h \times id)
\\=\;&(g + id) \circ dstl \circ (id \times h) \circ swap.
\end{alignat*}
% The application of \ref{law:uniformity} is justified by
% \begin{alignat*}{1}
% &(id + swap) \circ ((g \circ swap) + id) \circ dstr \circ (h \times id)
% \\=\;&(g + id) \circ (swap + swap) \circ dstr \circ (h \times id)
% \\=\;&(g + id) \circ dstl \circ swap \circ (h \times id)
% \\=\;&(g + id) \circ dstl \circ (id \times h) \circ swap.
% \end{alignat*}
This concludes one direction of the proof that left stability and right stability imply each other, the other direction follows symmetrically.
\end{proof}
@ -421,25 +420,44 @@ For the rest of this chapter we will assume every $KX$ to exist and be stable. U
Let us first introduce a proof principle similar to \autoref{rem:coinduction}.
\begin{remark}[Proof by right-stability]~\label{rem:proofbystability}
Given two morphisms $g, h : X \times KY \rightarrow A$ where $X, Y \in \obj{\C}, A \in \obj{\elgotalgs{\C}}$ to show that $g = h$ it suffices to show that $g$ and $h$ are right iteration preserving and there exists a morphism $f : X \times Y \rightarrow A$ such that $g \circ (id \times \eta) = f$ and $h \circ (id \times \eta) = f$.
Given two morphisms $g, h : X \times KY \rightarrow A$ where $X, Y \in \obj{\C}, A \in \obj{\elgotalgs{\C}}$. To show that $g = h$, it suffices to show that $g$ and $h$ are right iteration preserving and there exists a morphism $f : X \times Y \rightarrow A$ such that
% https://q.uiver.app/#q=WzAsMyxbMCwwLCJYIFxcdGltZXMgS1kiXSxbMiwwLCJBIl0sWzAsMiwiWCBcXHRpbWVzIFkiXSxbMCwxLCJnIiwwLHsib2Zmc2V0IjotMX1dLFswLDEsImgiLDIseyJvZmZzZXQiOjF9XSxbMiwxLCJmIiwyXSxbMiwwLCJpZCBcXHRpbWVzIFxcZXRhIl1d
\[\begin{tikzcd}[ampersand replacement=\&]
{X \times KY} \&\& A \\
\\
{X \times Y}
\arrow["g", shift left, from=1-1, to=1-3]
\arrow["h"', shift right, from=1-1, to=1-3]
\arrow["f"', from=3-1, to=1-3]
\arrow["{id \times \eta}", from=3-1, to=1-1]
\end{tikzcd}\]
commutes.
\end{remark}
Of course there is also a symmetric version of this.
\begin{remark}[Proof by left-stability]~\label{rem:proofbyleftstability}
Given two morphisms $g, h : X \times KY \rightarrow A$ where $X, Y \in \obj{\C}, A \in \obj{\elgotalgs{\C}}$ to show that $g = h$ it suffices to show that $g$ and $h$ are left iteration preserving and there exists a morphism $f : Y \times X \rightarrow A$ such that $g \circ (\eta \times id) = f$ and $h \circ (\eta \times id) = f$.
Given two morphisms $g, h : KX \times Y \rightarrow A$ where $X, Y \in \obj{\C}, A \in \obj{\elgotalgs{\C}}$. To show that $g = h$, it suffices to show that $g$ and $h$ are left iteration preserving and there exists a morphism $f : X \times Y \rightarrow A$ such that
% https://q.uiver.app/#q=WzAsMyxbMCwwLCJLWCBcXHRpbWVzIFkiXSxbMiwwLCJBIl0sWzAsMiwiWCBcXHRpbWVzIFkiXSxbMCwxLCJnIiwwLHsib2Zmc2V0IjotMX1dLFswLDEsImgiLDIseyJvZmZzZXQiOjF9XSxbMiwxLCJmIiwyXSxbMiwwLCJcXGV0YSBcXHRpbWVzIGlkIl1d
\[\begin{tikzcd}[ampersand replacement=\&]
{KX \times Y} \&\& A \\
\\
{X \times Y}
\arrow["g", shift left, from=1-1, to=1-3]
\arrow["h"', shift right, from=1-1, to=1-3]
\arrow["f"', from=3-1, to=1-3]
\arrow["{\eta \times id}", from=3-1, to=1-1]
\end{tikzcd}\]
commutes.
\end{remark}
\todo[inline]{Maybe do a helper proposition first that characterizes tau with the three laws in the file}
\begin{theorem}
$\mathbf{K}$ is a strong monad.
\end{theorem}
\begin{proof}
We define strength as $\tau = (\eta : X \times Y \rightarrow K(X \times Y))^\sharp : X \times KY \rightarrow K(X \times Y)$
We define strength as $\tau = \rs{(\eta : X \times Y \rightarrow K(X \times Y))} : X \times KY \rightarrow K(X \times Y)$. Note that $\tau$ is right iteration preserving by definition and $\tau \circ (id \times \eta) = \eta$.
\change[inline]{Maybe put complete proof}
Most of the requisite proofs will be done by right-stability, i.e.\ to prove an identity we need to give a unifying morphism such that the requisite diagram commutes, and we need to show that both sides of the identity are right iteration preserving. The proofs of commutativity follow by easy rewriting and are thus deferred to the formalization. The proofs of right iteration preservation follow in most cases instantly since the morphisms are composed of (right) iteration preserving morphisms but in non-trivial cases we will give the full proof.
To check naturality and the strength laws we will use \autoref{rem:proofbystability} and for brevity only state the needed unifying morphism by pasting \ref{sharpl1} into the required diagram. The proofs of \ref{sharpr1} and \ref{sharpr2} can then be looked up in the formalization.
For naturality of $\tau$ we use:
Naturality of $\tau$ follows by:
% https://q.uiver.app/#q=WzAsNSxbMSwwLCJBIFxcdGltZXMgS0IiXSxbMCwzLCJBIFxcdGltZXMgQiJdLFsxLDIsIksoQSBcXHRpbWVzIEIpIl0sWzMsMiwiSyhYIFxcdGltZXMgWSkiXSxbMywwLCJYIFxcdGltZXMgS1kiXSxbMSwwLCJpZCBcXHRpbWVzIFxcZXRhIiwwLHsiY3VydmUiOi0yfV0sWzAsMiwiXFx0YXUiLDJdLFsyLDMsIksoZlxcdGltZXMgZykiLDJdLFswLDQsImYgXFx0aW1lcyBLZyJdLFs0LDMsIlxcdGF1Il0sWzEsMywiXFxldGEgXFxjaXJjIChmIFxcdGltZXMgZykiLDIseyJjdXJ2ZSI6Mn1dXQ==
\[\begin{tikzcd}
& {A \times KB} && {X \times KY} \\
@ -453,10 +471,38 @@ Of course there is also a symmetric version of this.
\arrow["\tau", from=1-4, to=3-4]
\arrow["{\eta \circ (f \times g)}"', curve={height=12pt}, from=4-1, to=3-4]
\end{tikzcd}\]
The strength laws are proven similarly:
Notably, $\tau \circ (f \times Kg)$ is right iteration preserving, since for any $Z : \obj{\C}$ and $h : Z \rightarrow KY + Z$:
\begin{alignat*}{1}
&\tau \circ (f \times Kg) \circ (id \times h^\#)
\\=\;&\tau \circ (f \times ((Kg + id) \circ h)^\#)
\\=\;&((\tau + id) \circ dstl \circ (id \times ((Kg + id) \circ h)))^\# \circ (f \times id)
\\=\;&(((\tau \circ (f \times Kg)) + id) \circ dstl \circ (id \times h))^\#.\tag{\ref{law:uniformity}}
\end{alignat*}
% where uniformity is justified by
% \begin{alignat*}{1}
% &(id + (f \times id)) \circ \tau \circ ((f \times Kg) + id) \circ dstl \circ (id \times h)
% \\=\;&(\tau + id) \circ dstl \circ (id \times ((Kg + id) \circ h)) \circ (f \times id)
% \end{alignat*}
% Both sides of the identity are right iteration preserving, since for any $Z \in \obj{\C}$ and $h : Z \rightarrow KY + Z$:
% \begin{alignat*}{1}
% &K(f \times g) \circ \tau \circ (id \times h^\#)
% \\=\;&K(f \times g) \circ ((\tau + id) \circ dstl \circ (id \times h))^\#
% \\=\;&(((K(f \times g) \circ \tau) + id) \circ dstl \circ (id \times h))^\#
% \end{alignat*}
% and
% \begin{alignat*}{1}
% &\tau \circ (f \times Kg) \circ (id \times h^\#)
% \\=\;&\tau \circ (f \times (Kg \circ h)^\#)
% \\=\;&
% \end{alignat*}
Let us now check the strength laws.
\begin{itemize}
\item[\ref{S1}] This is an instance of the following more general law that holds on $\mathbf{K}$:
\item[\ref{S1}] Note that for $K\pi_2 \circ \tau = \pi_2$ holds more generally for any $X, Y \in \obj{\C}$, instead of just for $X = 1$:
% https://q.uiver.app/#q=WzAsNCxbMCwwLCJYIFxcdGltZXMgS1kiXSxbMiwwLCJLKFhcXHRpbWVzIFkpIl0sWzIsMiwiS1kiXSxbMCwyLCJYIFxcdGltZXMgWSJdLFswLDEsIlxcdGF1Il0sWzEsMiwiS1xccGlfMiJdLFswLDIsIlxccGlfMiIsMl0sWzMsMCwiaWQgXFx0aW1lcyBcXGV0YSIsMl0sWzMsMiwiXFxldGEgXFxjaXJjIFxccGlfMiIsMl1d
\[\begin{tikzcd}
{X \times KY} && {K(X\times Y)} \\
@ -469,9 +515,8 @@ Of course there is also a symmetric version of this.
\arrow["{\eta \circ \pi_2}"', from=3-1, to=3-3]
\end{tikzcd}\]
\item[\ref{S2}]
This is an instance of \ref{sharpr1}.
\item[\ref{S3}]
\item[\ref{S2}] As already mentioned, $\tau \circ (id \times \eta) = \eta$ follows by definition of $\tau$.
\item[\ref{S3}] To show that $\tau \circ (id \times \mu) = \tau^* \circ \tau$, consider:
% https://q.uiver.app/#q=WzAsNSxbMSwwLCJYIFxcdGltZXMgS0tZIl0sWzMsMCwiWCBcXHRpbWVzIEtZIl0sWzMsMiwiSyhYXFx0aW1lcyBZKSJdLFsxLDIsIksoWCBcXHRpbWVzIEtZKSJdLFswLDMsIlggXFx0aW1lcyBLWSJdLFswLDEsImlkIFxcdGltZXMgXFxtdSIsMl0sWzEsMiwiXFx0YXUiLDJdLFswLDMsIlxcdGF1Il0sWzMsMiwiXFx0YXVeKiJdLFs0LDAsImlkIFxcdGltZXMgXFxldGEiLDAseyJjdXJ2ZSI6LTJ9XSxbNCwyLCJcXHRhdSIsMCx7ImN1cnZlIjoyfV1d
\[\begin{tikzcd}
& {X \times KKY} && {X \times KY} \\
@ -485,7 +530,7 @@ Of course there is also a symmetric version of this.
\arrow["{id \times \eta}", curve={height=-12pt}, from=4-1, to=1-2]
\arrow["\tau", curve={height=12pt}, from=4-1, to=3-4]
\end{tikzcd}\]
\item[\ref{S4}]
\item[\ref{S4}] Lastly, consider the following diagram:
% https://q.uiver.app/#q=WzAsNixbMSwwLCIoWCBcXHRpbWVzIFkpIFxcdGltZXMgS1oiXSxbMSwyLCJYIFxcdGltZXMgWSBcXHRpbWVzIEtZIl0sWzMsMCwiSygoWCBcXHRpbWVzIFkpIFxcdGltZXMgWikiXSxbMywyLCJLKFggXFx0aW1lcyBZIFxcdGltZXMgWikiXSxbMiwyLCJYIFxcdGltZXMgSyhZIFxcdGltZXMgWikiXSxbMCwzLCIoWCBcXHRpbWVzIFkpIFxcdGltZXMgWiJdLFswLDEsIlxcYWxwaGEiXSxbMiwzLCJLXFxhbHBoYSJdLFswLDIsIlxcdGF1Il0sWzEsNCwiaWQgXFx0aW1lc1xcdGF1Il0sWzQsMywiXFx0YXUiXSxbNSwwLCJpZCBcXHRpbWVzIFxcZXRhIiwwLHsiY3VydmUiOi0yfV0sWzUsMywiXFxldGEgXFxjaXJjIFxcYWxwaGEiLDIseyJjdXJ2ZSI6Mn1dXQ==
\[\begin{tikzcd}
& {(X \times Y) \times KZ} && {K((X \times Y) \times Z)} \\
@ -500,9 +545,60 @@ Of course there is also a symmetric version of this.
\arrow["{id \times \eta}", curve={height=-12pt}, from=4-1, to=1-2]
\arrow["{\eta \circ \alpha}"', curve={height=12pt}, from=4-1, to=3-4]
\end{tikzcd}\]
where $\tau \circ (id \times \tau) \circ \alpha$ is right iteration preserving, since for any $Z : \obj{\C}$ and $h : Z \rightarrow KX + Z$:
\begin{alignat*}{1}
&\tau \circ (id \times \tau) \circ \alpha \circ (id \times h^\#)
\\=\;&\tau \circ \langle \pi_1 \circ \pi_1 , \tau \circ \langle \pi_2 \circ \pi_1 , \pi_2 \rangle \rangle \circ (id \times h^\#)
\\=\;&\tau \circ \langle \pi_1 \circ \pi_1 , \tau \circ \langle \pi_2 \circ \pi_1 , h^\# \circ \pi_2 \rangle \rangle
\\=\;&\tau \circ \langle \pi_1 \circ \pi_1 , \tau \circ (id \times h^\#) \circ \langle \pi_2 \circ \pi_1 , \pi_2 \rangle \rangle
\\=\;&\tau \circ \langle \pi_1 \circ \pi_1 , ((\tau + id) \circ dstl \circ (id \times h))^\# \circ \langle \pi_2 \circ \pi_1 , \pi_2 \rangle \rangle
\\=\;&\tau \circ (id \times ((\tau + id) \circ dstl \circ (id \times h))^\#) \circ \alpha
\\=\;&((\tau + id) \circ dstl \circ (id \times ((\tau + id) \circ dstl \circ (id \times h))))^\# \circ \alpha
\\=\;&(((\tau \circ (id \times \tau) \circ \alpha) + id) \circ dstl \circ (id \times h))^\#.\tag{\ref{law:uniformity}}
\end{alignat*}
\end{itemize}
\end{proof}
As we did when proving commutativity of $\mathbf{D}$, let us record some facts about $\tau$ and the induced $\sigma$, before proving commutativity of $\mathbf{K}$.
\begin{corollary}
$\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}
\end{alignat*}
\end{corollary}
\begin{proof}
Note that the first part of the proof amounts to showing that $\sigma = \ls{\eta}$ using uniqueness of $\ls{\eta}$. Indeed,
\begin{alignat*}{1}
&\sigma \circ (\eta \times id)
\\=\;&Kswap \circ \tau \circ swap \circ (\eta \times id)
\\=\;&Kswap \circ \tau \circ (id \times \eta) \circ swap
\\=\;&Kswap \circ \eta \circ swap
\\=\;&\eta \circ swap \circ swap
\\=\;&\eta
\end{alignat*}
and for any $h : Z \rightarrow KX + Z$
\begin{alignat*}{1}
&\sigma \circ (h^\# \times id)
\\=\;&Kswap \circ \tau \circ swap \circ (h^\# \times id)
\\=\;&Kswap \circ \tau \circ (id \times h^\#) \circ swap
\\=\;&Kswap \circ ((\tau + id) \circ dstl \circ (id \times h))^\# \circ swap
\\=\;&(((Kswap \circ \tau) + id) \circ dstl \circ (id \times h))^\# \circ swap
\\=\;&((\sigma + id) \circ dstr \circ (h \times id))^\#.\tag{\ref{law:uniformity}}
\end{alignat*}
Let us now proceed with the properties of $\tau$ and $\sigma$.
\begin{itemize}
\item[(\ref{Ktau1})]
\begin{alignat*}{1}
todo
\end{alignat*}
\end{itemize}
\end{proof}
\begin{theorem}
$\mathbf{K}$ is a commutative monad.
\end{theorem}
@ -550,9 +646,6 @@ Of course there is also a symmetric version of this.
We need to show that $\tau \circ \Delta = K \langle \eta , id \rangle$. Note that $K \langle \eta , id \rangle = \free{\eta \circ \langle \eta , id \rangle}$, which is a unique Elgot algebra morphism satisfying $K \langle \eta , id \rangle \circ \eta = \eta \circ \langle \eta , id \rangle$. It thus suffices to show that $\tau \circ \Delta$ satisfies the same identity and is iteration preserving.
The identity follows easily
\todo[inline]{Reference $\tau-\eta$ in last step:}
\begin{alignat*}{1}
&\tau \circ \Delta \circ \eta
\\=\;&\tau \circ \langle \eta , \eta \rangle
@ -585,6 +678,6 @@ Of course there is also a symmetric version of this.
$\mathbf{K}$ is the initial (strong) pre-Elgot monad.
\end{theorem}
\begin{proof}
Note that $\mathbf{K}$ is by definition a pre-Elgot monad.
Note that $\mathbf{K}$ is a pre-Elgot monad by definition.
\todo[inline]{Proof that K is initial strong pre-Elgot}
\end{proof}