diff --git a/thesis/main.tex b/thesis/main.tex index aa0e381..9e54e45 100644 --- a/thesis/main.tex +++ b/thesis/main.tex @@ -101,7 +101,6 @@ \usepackage{mathpartir} \newcommand{\obj}[1]{\ensuremath{\vert \mathcal{#1} \vert}} - \begin{document} \pagestyle{plain} \input{src/titlepage}% diff --git a/thesis/src/01_preliminaries.tex b/thesis/src/01_preliminaries.tex index 36ebbac..a4f51da 100644 --- a/thesis/src/01_preliminaries.tex +++ b/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. -Other notions that are crucial to this thesis will be introduced in this section. -In the following sections we will work in an ambient category that is distributive and has a parametrized natural numbers object $\mathbb{N}$. +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. +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. +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} - % TODO add quantifiers - \item $\mu_X \circ \mu_{FX} = \mu_X \circ F\mu_X$ - \item $\mu_X \circ \eta_{FX} = id_{FX}$ - \item $\mu_X \circ F\eta_X = id_{FX}$ - \end{enumerate} + \begin{alignat*}{1} + &\mu_X \circ \mu_{FX} = \mu_X \circ F\mu_X \tag*{(M1)}\label{M1}\\ + &\mu_X \circ \eta_{FX} = id_{FX} \tag*{(M2)}\label{M2}\\ + &\mu_X \circ F\eta_X = id_{FX} \tag*{(M3)}\label{M3} + \end{alignat*} \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} - % TODO add quantifiers - \item $\eta_X^* = id_{FX}$ - \item $\eta_X \circ f^* = f$ - \item $f^* \circ g* = (f \circ g^*)^*$ - \end{enumerate} + \begin{alignat*}{1} + &\eta_X^* = id_{FX} \tag*{(K1)}\label{K1}\\ + &\eta_X \circ f^* = f \tag*{(K2)}\label{K2}\\ + &f^* \circ g* = (f \circ g^*)^* \tag*{(K3)}\label{K3} + \end{alignat*} \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} - \item $M\pi_2 \circ \tau_{1,X} = \pi_2$ - \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}$ - \item $\tau_{X,Y} \circ (id_X \times \eta_Y) = \eta_{X\times Y}$ - \item $\tau_{X,Y} \circ (id_X \times \mu_Y) = \mu_{X\times Y} \circ M\tau_{X,Y} \circ \tau_{X,MY}$ -\end{enumerate} + \begin{alignat*}{1} + &M\pi_2 \circ \tau_{1,X} = \pi_2 \tag*{(S1)}\label{S1}\\ + &\tau_{X,Y} \circ (id_X \times \eta_Y) = \eta_{X\times Y} \tag*{(S2)}\label{S2}\\ + &\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}\\ + &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{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: diff --git a/thesis/src/03_partiality-monads.tex b/thesis/src/03_partiality-monads.tex index 08549ce..73bff90 100644 --- a/thesis/src/03_partiality-monads.tex +++ b/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} - f \circ (\tdom f) &= f\\ - (\tdom f) \circ (\tdom g) &= (\tdom g) \circ (\tdom f)\\ - \tdom(g \circ (\tdom f)) &= (\tdom g) \circ (\tdom f)\\ - (\tdom h) \circ f &= f \circ \tdom (h \circ f) - \end{alignat} + \begin{alignat*}{1} + f \circ (\tdom f) &= f\tag*{(R1)}\\ + (\tdom f) \circ (\tdom g) &= (\tdom g) \circ (\tdom f)\tag*{(R2)}\\ + \tdom(g \circ (\tdom f)) &= (\tdom g) \circ (\tdom f)\tag*{(R3)}\\ + (\tdom h) \circ f &= f \circ \tdom (h \circ f)\tag*{(R4)} + \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: + + \[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 \] + + \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}. + \end{itemize} +\end{proof} - Choose $now : X \rightarrow DX$ and given $f : X \rightarrow DY$ we define $f^* =\; ! \circ i_1$ by: - - % https://q.uiver.app/#q=WzAsNSxbMCwxLCJEWCArIERZIl0sWzYsMSwiWSArIChEWCArIERZKSJdLFswLDAsIkRYIl0sWzAsMiwiRFkiXSxbNiwyLCJZICsgRFkiXSxbMCwxLCJbIFsgWyBp4oKBICwgaeKCgiDiiJggaeKCgiBdIOKImCAob3V0IOKImCBmKSAsIGnigoIg4oiYIGnigoEgXSDiiJggb3V0ICwgKGlkQyAr4oKBIGnigoIpIOKImCBvdXQgXSJdLFsyLDAsImlfMSJdLFswLDMsIiEiLDAseyJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJkYXNoZWQifX19XSxbMyw0LCJvdXQiXSxbMSw0LCJGICEiLDAseyJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJkYXNoZWQifX19XV0= +Since $DX$ is a final coalgebra we get the following proof principle: +\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=WzAsOCxbMCwwLCJYIl0sWzAsMSwiRFkiXSxbMiwxLCJZICsgRFkiXSxbMiwwLCJZICsgWCJdLFs0LDAsIlgiXSxbNCwxLCJEWSJdLFs2LDAsIlkgKyBYIl0sWzYsMSwiWSArIERZIl0sWzEsMiwib3V0Il0sWzAsMywiXFxhbHBoYSJdLFswLDEsImYiXSxbMywyLCJpZCArIGYiXSxbNCw2LCJcXGFscGhhIl0sWzQsNSwiZyJdLFs2LDcsImlkICsgZyJdLFs1LDcsIm91dCIsMl1d \[\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-7] - \arrow["{i_1}", from=1-1, to=2-1] - \arrow["{!}", dashed, from=2-1, to=3-1] - \arrow["out", from=3-1, to=3-7] - \arrow["{F !}", dashed, from=2-7, to=3-7] + 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} \ No newline at end of file