Finishing touches on partiality chapter

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

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}                         \\
+    f \circ (\tdom f)         & = f                         \\
-    (\tdom f) \circ (\tdom g) & = (\tdom g) \circ (\tdom f)\tag*{(R2)}\label{R2} \\
+    (\tdom f) \circ (\tdom g) & = (\tdom g) \circ (\tdom f) \\
-    \tdom(g \circ (\tdom f))  & = (\tdom g) \circ (\tdom f)\tag*{(R3)}\label{R3} \\
+    \tdom(g \circ (\tdom f))  & = (\tdom g) \circ (\tdom f) \\
-    (\tdom h) \circ f         & = f \circ \tdom (h \circ f)\tag*{(R4)}\label{R4}
+    (\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}
+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:
-  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:
 
 \[
   (\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^*\]
+          It follows that indeed \[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)\).
+    \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:
+  It suffices to show \({[ now , f ]}^* = {[ now , i ]}^*\), because then follows that
-  \[f = {[ now , f ]}^* \circ g = {[ now , i ]}^* \circ g = i\]
+  \[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 \]
+  \[\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 \]
+  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}