From be09d767ea7242aed270ff44eb0ec75fb3b876da Mon Sep 17 00:00:00 2001 From: Leon Vatthauer Date: Mon, 26 Feb 2024 15:06:51 +0100 Subject: [PATCH] improve proves in delay chapter --- thesis/src/01_preliminaries.tex | 70 ++++++++- thesis/src/03_partiality-monads.tex | 211 +++++++++++++++++----------- 2 files changed, 193 insertions(+), 88 deletions(-) diff --git a/thesis/src/01_preliminaries.tex b/thesis/src/01_preliminaries.tex index cd3acd8..579ac35 100644 --- a/thesis/src/01_preliminaries.tex +++ b/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] - \label{def:distributive} +\begin{definition}[Distributive Category]~\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: diff --git a/thesis/src/03_partiality-monads.tex b/thesis/src/03_partiality-monads.tex index 7804bb8..a33a9f1 100644 --- a/thesis/src/03_partiality-monads.tex +++ b/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\] - and - \[i_2 \;\circ \;! = (id\;+\;!) \circ dstl \circ \langle i_2 , i_2 \rangle\] - which follow easily by the facts that - \[dstl \circ (id \times i_1) = i_1\] - and - \[dstl \circ (id \times i_2) = i_2\] - that are both proven by monicity of $dstl^{-1}$. + + This is easily proven by pre-composing with $i_1$ and $i_2$: + \begin{alignat*}{1} + &(id\;+\;!) \circ dstl \circ \langle i_1 , i_1 \rangle + \\=\;&(id\;+\;!) \circ dstl \circ (id \times i_1) \circ \langle i_1 , id \rangle + \\=\;&(id\;+\;!) \circ i_1 \circ \langle i_1 , id \rangle + \\=\;&i_1 \circ \langle i_1 , id \rangle + \end{alignat*} + + \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} - \label{col:delay} +\begin{proposition}~\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$. - Then $[ g , id ] : DX + DY \rightarrow DY$ is a coalgebra morphism and thus $[ g , id ] =\;\coalg{\alpha}$ by uniqueness of $\coalg{\alpha}$. + \begin{alignat*}{1} + &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] - \label{rem:coinduction} +\begin{remark}[Proof by 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: - \begin{alignat*}{1} - &out \circ Df = (f + Df) \circ out - \\&later \circ f^* = (later \circ f)^* = f^* \circ later - \end{alignat*} + The following properties hold: + \begin{alignat}{1} + &out \circ Df = (f + Df) \circ out\label{eq:outD} + \\&f^* = [ f , {(later \circ f)}^* ] \circ out\label{eq:f*help} + \\&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: - - \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*} + We prove them one by one: \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}. + \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*} + \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}] - \todo[inline]{What to do about out-law?} - \begin{alignat*}{1} - & out \circ Dswap \circ \tau \circ swap - \\=\;&(swap + Dswap) \circ out \circ \tau \circ swap - \\=\;&(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{sigma2}] + \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}] By monicity of $out$: + \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 ] , 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 [ \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 f ] ] \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}} + \\=\; & [ 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 , {[ 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 \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?}