diff --git a/agda/src/Monad/Instance/K/Commutative.lagda.md b/agda/src/Monad/Instance/K/Commutative.lagda.md index 6d3aea8..ea9a73e 100644 --- a/agda/src/Monad/Instance/K/Commutative.lagda.md +++ b/agda/src/Monad/Instance/K/Commutative.lagda.md @@ -125,6 +125,7 @@ private where f' = (η _ +₁ idC) ∘ f g' = (η _ +₁ idC) ∘ g + w : X × Z ⇒ monadK.F.F₀ (X × K.₀ U + K.₀ Y × Z) + X × Z w = [ i₁ ∘ K.₁ i₁ ∘ τ _ , (K.₁ i₂ ∘ σ _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (f' ⁂ idC) ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ g') w-law₁ : f' # ∘ π₁ ≈ extend [ f' # ∘ π₁ , η _ ∘ π₁ ] ∘ w # w-law₁ = sym (begin diff --git a/thesis/src/04_partiality-monads.tex b/thesis/src/04_partiality-monads.tex index 3666f04..5db03d2 100644 --- a/thesis/src/04_partiality-monads.tex +++ b/thesis/src/04_partiality-monads.tex @@ -21,23 +21,15 @@ To ensure that programs are partial, we recall the following notion by Cockett a \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\tag*{(R1)}\label{R1} \\ - (\tdom f) \circ (\tdom g) & = (\tdom g) \circ (\tdom f)\tag*{(R2)}\label{R2} \\ - \tdom(g \circ (\tdom f)) & = (\tdom g) \circ (\tdom f)\tag*{(R3)}\label{R3} \\ - (\tdom h) \circ f & = f \circ \tdom (h \circ f)\tag*{(R4)}\label{R4} + 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*} for any \(X, Y, Z \in \vert\mathcal{C}\vert, f : X \rightarrow Y, g : X \rightarrow Z, h: Y \rightarrow Z\). \end{definition} -\begin{lemma} - For any \(f : X \rightarrow Y\) the restriction morphism \(\tdom f\) is idempotent. -\end{lemma} -\begin{proof} - This follows by~\ref{R3} and~\ref{R1}: - \[\tdom f \circ \tdom f = \tdom (f \circ \tdom f) = \tdom f\tag*{\qedhere}\] -\end{proof} - -The idempotent morphism \(\tdom f : X \rightarrow X\) represents the domain of definiteness of \(f : X \rightarrow Y\). In the category of partial functions this takes the following form: +The morphism \(\tdom f : X \rightarrow X\) represents the domain of definiteness of \(f : X \rightarrow Y\). In the category of partial functions this takes the following form: \[ (\tdom f)(x) = \begin{cases} @@ -55,7 +47,7 @@ That is, \(\tdom f\) is only defined on values where \(f\) is defined and for th For a suitable defined partiality monad \(T\) the Kleisli category \(\C^T\) should be a restriction category. -Lastly we also recall the following notion by Bucalo et al.~\cite{eqlm} which captures what it means for a monad to have no other side effect besides some sort of non-termination: +Lastly, we also recall the following notion by Bucalo et al.~\cite{eqlm} which captures what it means for a monad to have no other side effect besides some sort of non-termination: \begin{definition}[Equational Lifting Monad]\label{def:eqlm} A commutative monad \(T\) is called an \textit{equational lifting monad} if the following diagram commutes: @@ -110,7 +102,7 @@ The endofunctor \(MX = X + 1\) extends to a monad by taking \(\eta_X = i_1 : X \ & (id + !) \circ dstl \circ (id \times (f + id)) \\ = \; & (id + !) \circ ((id \times f) + (id \times id)) \circ dstl \\ = \; & ((id \times f) + !) \circ dstl \\ - = \; & ((id \times f) + id) \circ (id + !) \circ dstl + = \; & ((id \times f) + id) \circ (id + !) \circ dstl. \end{alignat*} The other strength laws and commutativity can be proven by using simple properties of distributive categories, we added these proofs to the formalization for completeness. @@ -131,20 +123,20 @@ The endofunctor \(MX = X + 1\) extends to a monad by taking \(\eta_X = i_1 : X \ \end{tikzcd} \] - This is easily proven by pre-composing with \(i_1\) and \(i_2\): + This is easily proven by pre-composing with \(i_1\) and \(i_2\), indeed \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 + \\=\;&i_1 \circ \langle i_1 , id \rangle, \end{alignat*} - + and \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 \; !\tag*{\qedhere} + \\=\;&i_2 \;\circ \; !.\tag*{\qedhere} \end{alignat*} \end{proof} @@ -152,7 +144,7 @@ In the setting of classical mathematics this monad is therefore sufficient for m \section{The Delay Monad} Capretta's delay monad~\cite{delay} is a coinductive datatype whose inhabitants can be viewed as suspended computations. -This datatype is usually defined by the two coinductive constructors \(now : X \rightarrow D\;X\) and \(later : D\;X \rightarrow D\;X\), where \(now\) is for lifting a value inside a computation and \(later\) intuitively delays a computation by one time unit. See \autoref{chp:setoids} or~\cite{delay}, for a type theoretical study of this monad. +This datatype is usually defined by the two coinductive constructors \(now : X \rightarrow DX\) and \(later : DX \rightarrow DX\), where \(now\) is for lifting a value inside a computation and \(later\) intuitively delays a computation by one time unit. See \autoref{chp:setoids} for a type theoretical study of this monad. Categorically we obtain the delay monad by the final F-coalgebras \(DX = \nu A. X + A\), which we assume to exist. In this section we will show that these final F-coalgebras indeed yield a monad that is strong and commutative. Since \(DX\) is defined as a final coalgebra, we can define morphisms via corecursion and prove theorems by coinduction. By \autoref{lem:lambek} 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\). @@ -225,14 +217,13 @@ Since \(DX\) is defined as a final coalgebra, we can define morphisms via corecu \\=\;&(id + \coalg{\alpha} \circ i_2) \circ out \end{alignat*} Let us verify that \(f^*\) indeed satisfies the requisite property: - \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 + \\=\;&[ 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\). @@ -245,39 +236,39 @@ Since \(DX\) is defined as a final coalgebra, we can define morphisms via corecu \\=\;&[ [ [ 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 ] + \\=\;&(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)\). + It follows that indeed \[g = [ g , id ] \circ i_1 =\;\coalg{\alpha} \circ i_1 = f^*.\] + \item[\ref{D3}] Take \(\tau := \coalg{dstl \circ (id \times out)} : X \times DY \rightarrow D(X \times Y)\), the requisite property then follows by definition. \qedhere \end{itemize} \end{proof} \begin{lemma} - The following properties follow from \autoref{lem:delay}: + The following properties of \(\mathbf{D}\) hold: \begin{enumerate} \item \(out \circ Df = (f + Df) \circ out\) \item \(f^* = [ f , {(later \circ f)}^* ] \circ out\) \item \(later \circ f^* = {(later \circ f)}^* = f^* \circ later\) \end{enumerate} \end{lemma} -\begin{proof} +\begin{proof} These identities follow by use of \autoref{lem:delay}: \begin{itemize} \item[1.] Note that definitionally: \(Df = {(now \circ f)}^*\) for any \(f : X \rightarrow TY\). The statement is then simply a consequence of~\ref{D1} and~\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}} + \\=\;&(f + Df) \circ out.\tag*{\ref{D1}} \end{alignat*} \item[2.] 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}} + \\=\;&[out \circ f , i_2 \circ [ f , {(later \circ f)}^* ] \circ out ] \circ out.\tag*{\ref{D1}} \end{alignat*} \item[3.] These equations follow by monicity of \(out\): @@ -290,7 +281,7 @@ Since \(DX\) is defined as a final coalgebra, we can define morphisms via corecu \\=\;&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}} + \\=\;&out \circ f^* \circ later. \tag*{\ref{D2}} \end{alignat*} \end{itemize} Thus, the postulated properties have been proven. @@ -300,7 +291,7 @@ Since \(DX\) is defined as a final coalgebra, we can define morphisms via corecu \(\mathbf{D} = (D, now, {(-)}^*)\) is a Kleisli triple. \end{theorem} \begin{proof} - We will now use the properties proven in Corollary~\ref{lem:delay} to prove the Kleisli triple laws: + We will now use the properties proven in \autoref{lem:delay} to prove the Kleisli triple laws: \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}. @@ -309,7 +300,7 @@ Since \(DX\) is defined as a final coalgebra, we can define morphisms via corecu & out \circ f^* \circ now \\=\;&[ out \circ f , i_2 \circ f^* ] \circ out \circ now\tag*{\ref{D2}} \\=\;&[ out \circ f , i_2 \circ f^* ] \circ i_1\tag*{\ref{D1}} - \\=\;&out \circ f + \\=\;&out \circ f. \end{alignat*} \item[\ref{K3}] Let \(f : Y \rightarrow Z, g : X \rightarrow Z\) to show \(f^* \circ g^* = {(f^* \circ g)}^*\) by uniqueness of \({(f^* \circ g)}^*\) it suffices to show: \begin{alignat*}{1} @@ -317,7 +308,7 @@ Since \(DX\) is defined as a final coalgebra, we can define morphisms via corecu \\=\;&[ out \circ f , i_2 \circ f^* ] \circ out \circ g^*\tag*{\ref{D2}} \\=\;&[ out \circ f , i_2 \circ f^* ] \circ [ out \circ g , i_2 \circ g^* ] \circ out\tag*{\ref{D2}} \\=\;&[ [ out \circ f , i_2 \circ f^* ] \circ out \circ g , i_2 \circ f^* \circ g^* ] \circ out - \\=\;&[ out \circ f^* \circ g , i_2 \circ f^* \circ g^* ] \circ out\tag*{\ref{D2}} + \\=\;&[ out \circ f^* \circ g , i_2 \circ f^* \circ g^* ] \circ out.\tag*{\ref{D2}} \end{alignat*} \end{itemize} This concludes the proof. @@ -386,19 +377,18 @@ Finality of the coalgebras \({(DX, out : DX \rightarrow X + DX)}_{X \in \obj{\C} \arrow["{\pi_2 + id}", from=1-3, to=1-4] \end{tikzcd} \] - \item[\ref{S2}] We don't need coinduction to show \(\tau \circ (id \times now) = now\), but we need a small helper lemma: + \item[\ref{S2}] We don't need coinduction to show \(\tau \circ (id \times now) = now\), but we will first need to establish \begin{equation*} - \tau \circ (id \times out^{-1}) = out^{-1} \circ (id + \tau) \circ dstl \tag*{(\(\ast \))}\label{helper} + \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: + With this we are done by \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 + =\; & now. \end{alignat*} - where the last step follows by \(dstl \circ (id \times i_1) = i_1\). \item[\ref{S3}] We need to check \(\tau^* \circ \tau = \tau \circ (id \times id^*)\), the coalgebra for coinduction is: % https://q.uiver.app/#q=WzAsNixbMCwwLCJYIFxcdGltZXMgRERZIl0sWzAsMiwiRChYXFx0aW1lcyBZKSJdLFsxLDAsIlggXFx0aW1lcyAoRFkgKyBERFkpIl0sWzIsMCwiWCBcXHRpbWVzIERZICsgWCBcXHRpbWVzIEREWSJdLFsyLDIsIlggXFx0aW1lcyBZICsgRChYIFxcdGltZXMgWSkiXSxbMiwxLCJYIFxcdGltZXMgWSArIFggXFx0aW1lcyBERFkiXSxbMCwxLCJcXGNvYWxney19IiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiZGFzaGVkIn19fV0sWzAsMiwiaWQgXFx0aW1lcyBvdXQiXSxbMiwzLCJkc3RsIl0sWzEsNCwib3V0Il0sWzUsNCwiaWQgKyBcXGNvYWxney19IiwyXSxbMyw1LCJbIChpZCArIChpZCBcXHRpbWVzIG5vdykpIFxcY2lyYyBkc3RsIFxcY2lyYyAoaWQgXFx0aW1lcyBvdXQpICwgaV8yIF0iLDJdXQ== \[ @@ -456,8 +446,8 @@ To prove that \(\mathbf{D}\) is commutative we will use another proof principle \end{corollary} \begin{proof} Let \(g : X \rightarrow D(Y + X)\) be guarded by \(h : X \rightarrow Y + D(Y+X)\) and \(f, i : X \rightarrow DY\) be solutions of g. - It suffices to show \({[ now , f ]}^* = {[ now , i ]}^*\), because then follows: - \[f = {[ now , f ]}^* \circ g = {[ now , i ]}^* \circ g = i\] + It suffices to show \({[ now , f ]}^* = {[ now , i ]}^*\), because then follows that + \[f = {[ now , f ]}^* \circ g = {[ now , i ]}^* \circ g = i.\] This is proven by coinduction using % https://q.uiver.app/#q=WzAsNSxbMCwxLCJEWSJdLFszLDEsIlkgKyBEWSJdLFswLDAsIkQoWSArIFgpIl0sWzEsMCwiKFkgKyBYKSArIEQoWStYKSJdLFszLDAsIlkgKyBEKFkrWCkiXSxbMCwxLCJvdXQiXSxbMiwzLCJvdXQiXSxbMyw0LCJbIFsgaV8xICwgaCBdICwgaV8yIF0iXSxbNCwxLCJpZCArIFxcY29hbGd7LX0iXSxbMiwwLCJcXGNvYWxney19IiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiZGFzaGVkIn19fV1d \[ @@ -489,7 +479,7 @@ Let us record some facts that we will use to prove commutativity of \(\mathbf{D} \begin{proof} \begin{itemize} \item[\ref{tau1}] This is just~\ref{D3} restated. - \item[\ref{sigma1}] + \item[\ref{sigma1}] Indeed, by use of~\ref{tau1} \begin{alignat*}{1} & out \circ \sigma \\=\;&out \circ Dswap \circ \tau \circ swap @@ -497,19 +487,19 @@ Let us record some facts that we will use to prove commutativity of \(\mathbf{D} \\=\;&(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) + \\=\;&(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 + \\=\;&(id + \tau) \circ dstl. \end{alignat*} - \item[\ref{sigma2}] By monicity of \(out\): + \item[\ref{sigma2}] Again, 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\tag*{\qedhere} + \\=\;&(id + \sigma) \circ dstr.\tag*{\qedhere} \end{alignat*} \end{itemize} \end{proof} @@ -521,27 +511,28 @@ Let us record some facts that we will use to prove commutativity of \(\mathbf{D} 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\] + \[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.\] \(g\) is trivially guarded by \([ id + D i_1 \circ \sigma , i_2 \circ [ D i_1 \circ \tau , later \circ now \circ i_2 ] ] \circ w\). - We are left to show that both \(\tau^* \circ \sigma \) and \(\sigma^* \circ \tau \) are solutions of \(g\). Consider: + We are left to show that both \(\tau^* \circ \sigma \) and \(\sigma^* \circ \tau \) are solutions of \(g\). Consider - \[\tau^* \circ \sigma = out^{-1} \circ [ id + \sigma , i_2 \circ [ \tau , later \circ \tau^* \circ \sigma ] ] \circ w = {[ now , \tau^* \circ \sigma]}^* \circ g \] - \[\sigma^* \circ \tau = out^{-1} \circ [ id + \sigma , i_2 \circ [ \tau , later \circ \sigma^* \circ \tau ] ] \circ w = {[ now , \sigma^* \circ \tau]}^* \circ g \] + \[\tau^* \circ \sigma = out^{-1} \circ [ id + \sigma , i_2 \circ [ \tau , later \circ \tau^* \circ \sigma ] ] \circ w = {[ now , \tau^* \circ \sigma]}^* \circ g, \] + and + \[\sigma^* \circ \tau = out^{-1} \circ [ id + \sigma , i_2 \circ [ \tau , later \circ \sigma^* \circ \tau ] ] \circ w = {[ now , \sigma^* \circ \tau]}^* \circ g. \] - The last step in both equations can be proven generally for any \(f : DX \times DY \rightarrow D(X \times Y)\) using monicity of \(out\): + The last step in both equations can be proven generally for any \(f : DX \times DY \rightarrow D(X \times Y)\) using 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 + \\=\; & [ id + \sigma , i_2 \circ [ \tau , later \circ f ] ] \circ w. \end{alignat*} 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\): + Again, we proceed by monicity of \(out\), which yields \begin{alignat*}{1} & out \circ \sigma^* \circ \tau \\=\;&[ out \circ \sigma , i_2 \circ \sigma^* ] \circ out \circ \tau\tag*{\ref{D2}} @@ -557,18 +548,17 @@ Let us record some facts that we will use to prove commutativity of \(\mathbf{D} \\=\;&[ (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 + \\=\;&[ (id + \sigma), i_2 \circ [ \tau , later \circ \sigma^* \circ \tau]] \circ w, \end{alignat*} - where \[Ddstr \circ \tau = [ Di_1 \circ \tau , Di_2 \circ \tau ] \circ dstr \tag*{(*)}\label{Dcomm-helper}\] - is proven using epicness of \(dstr^{-1}\): + indeed follows by epicness of \(dstr^{-1}\): \begin{alignat*}{1} & Ddstr \circ \tau \circ dstr^{-1} \\=\;&[ Ddstr \circ \tau \circ (i_1 \times id) , Ddstr \circ \tau \circ (i_2 \times id) ] \\=\;&[ 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 ]\tag*{\qedhere} + \\=\;&[ Di_1 \circ \tau , Di_2 \circ \tau ].\tag*{\qedhere} \end{alignat*} \end{proof}