minor updates

sofp-src/sofp-applicative.lyx

@@ -22870,15 +22870,15 @@ noprefix "false"
 \end_layout
 
 \begin_layout Standard
-We conclude this section with a proof of the 
+We conclude this section with a proof of one version of the 
 \begin_inset Quotes eld
 \end_inset
 
 unrolling trick
 \begin_inset Quotes erd
 \end_inset
 
-.
+ for recursive types:
 \begin_inset Index idx
 status collapsed
 
@@ -26190,7 +26190,7 @@ If
 F^{A}\times Z & \_^{:F^{A}}\times z\rightarrow z & \bbnum 0\\
 Z\times F^{B} & z\times\_^{:F^{B}}\rightarrow z & \bbnum 0\\
 F^{A}\times F^{B} & \bbnum 0 & \text{zip}_{F}
-\end{array}\quad;
+\end{array}\quad.
 \end{align*}
 
 \end_inset
@@ -27150,7 +27150,7 @@ toF
 
 \end_inset
 
-For profunctors, the identity laws of 
+For profunctors, the right identity law of 
 \begin_inset listings
 inline true
 status open
@@ -27174,15 +27174,15 @@ pure
 
 \end_inset
 
- have the form:
+ has the form:
 \begin_inset Formula 
 \[
 \text{zip}_{F}(a^{:F^{A}}\times\text{pu}_{F}(b^{:B}))=a\triangleright(k^{:A}\rightarrow k\times b)^{\uparrow F}\pi_{1}^{\downarrow F}\quad.
 \]
 
 \end_inset
 
-So, we can rewrite the left-hand side of the associativity law:
+So, we can rewrite the left-hand side of the associativity law like this:
 \begin_inset Formula 
 \begin{align*}
 \text{left-hand side}:\quad & \text{zip}_{P}(p\times\text{zip}_{P}(q\times r))\triangleright\varepsilon_{1,23}^{\uparrow P}\tilde{\varepsilon}_{1,23}^{\downarrow P}=\bbnum 0+\gunderline{\text{zip}_{F}}\big(a\times\gunderline{\text{pu}_{F}}(\text{ex}_{H}(b)\times\text{ex}_{H}(c))\big)\triangleright\varepsilon_{1,23}^{\uparrow F}\tilde{\varepsilon}_{1,23}^{\downarrow F}\\