add build script

.github/workflows/build-pdf.yml

@@ -30,7 +30,7 @@ jobs:
         id: full-pdf
         uses: docker://winitzki/sofp-docker-build:latest
         with:
-          args: "LYXDIR=/root/.lyx bash sofp-src/scripts/make_all.sh"
+          args: "LYXDIR=/root/.lyx bash sofp-src/make_sofp_pdf.sh"
 
       - name: Upload built PDF
         id: upload-pdf

sofp-src/lyx/sofp-free-type.lyx

@@ -34778,25 +34778,15 @@ recursive
 status open
 
 \begin_layout Plain Layout
-This 
-\begin_inset Quotes eld
-\end_inset
-
-Church encoding
-\begin_inset Quotes erd
-\end_inset
-
- is known more precisely as 
+The 
 \begin_inset Quotes eld
 \end_inset
 
 Boehm-Berarducci encoding
 \begin_inset Quotes erd
 \end_inset
 
-.
- For the purposes of this book, they are the same.
- See 
+ discussed in 
 \family typewriter
 
 \begin_inset CommandInset href
@@ -34808,7 +34798,7 @@ literal "false"
 
 
 \family default
- for discussion.
+ can be seen as a curried form of the Church encoding.
 \end_layout
 
 \end_inset
@@ -34910,18 +34900,10 @@ noprefix "false"
 \begin_layout Standard
 The following statement
 \begin_inset Foot
-status collapsed
+status open
 
 \begin_layout Plain Layout
 See also the papers 
-\begin_inset Quotes eld
-\end_inset
-
-A note on strong dinaturality
-\begin_inset Quotes erd
-\end_inset
-
- (
 \family typewriter
 
 \begin_inset CommandInset href
@@ -34934,15 +34916,7 @@ literal "false"
 
 
 \family default
-) and 
-\begin_inset Quotes eld
-\end_inset
-
-Build, augment, and destroy universally
-\begin_inset Quotes erd
-\end_inset
-
- (
+ and 
 \family typewriter
 
 \begin_inset CommandInset href
@@ -34954,7 +34928,7 @@ literal "false"
 
 
 \family default
-).
+.
 \end_layout
 
 \end_inset
@@ -35241,6 +35215,26 @@ fix
 
 \end_inset
 
+Omitting type annotations, we may write 
+\begin_inset listings
+inline true
+status open
+
+\begin_layout Plain Layout
+
+fix
+\end_layout
+
+\end_inset
+
+ as:
+\begin_inset Formula 
+\[
+\text{fix}\triangleq f\rightarrow\,^{Y}\rightarrow q\rightarrow f\triangleright(p\rightarrow q\triangleright p^{Y})^{\uparrow F}\bef q\quad.
+\]
+
+\end_inset
+
 
 \end_layout
 
@@ -35537,7 +35531,8 @@ It remains to verify that the last line holds.
 \begin_inset Formula 
 \begin{align*}
  & \text{fix}^{\uparrow F}\bef f\overset{?}{=}f^{\uparrow F}\bef q\quad,\\
-\text{or equivalently}:\quad & \text{fix}^{\uparrow F}\bef\big(p^{:\forall X.\,(F^{X}\rightarrow X)\rightarrow X}\rightarrow q\triangleright p^{Y}\big)^{\uparrow F}\bef q\overset{?}{=}\big(p^{:\forall X.\,(F^{X}\rightarrow X)\rightarrow X}\rightarrow q\triangleright p^{Y}\big)^{\uparrow F\uparrow F}\bef q^{\uparrow F}\bef q\quad.
+\text{or equivalently}:\quad & \text{fix}^{\uparrow F}\bef\big(p^{:\forall X.\,(F^{X}\rightarrow X)\rightarrow X}\rightarrow q\triangleright p^{Y}\big)^{\uparrow F}\bef q\\
+ & \quad\overset{?}{=}\big(p^{:\forall X.\,(F^{X}\rightarrow X)\rightarrow X}\rightarrow q\triangleright p^{Y}\big)^{\uparrow F\uparrow F}\bef q^{\uparrow F}\bef q\quad.
 \end{align*}
 
 \end_inset
@@ -35656,27 +35651,75 @@ noprefix "false"
 \begin_inset Formula $f$
 \end_inset
 
- by
+ by:
 \begin_inset Formula 
 \[
-r\triangleq\text{fix}^{\uparrow F}\quad,\quad\quad f\triangleq u^{:F^{T}}\rightarrow s\triangleright(u\triangleright\text{fix})\quad.
+r\triangleq\text{fix}^{\uparrow F}\quad,\quad\quad f\triangleq u^{:F^{T}}\rightarrow s\triangleright(u\triangleright\text{fix})^{B}\quad.
 \]
 
 \end_inset
 
+Substituting the definition of 
+\begin_inset listings
+inline true
+status open
+
+\begin_layout Plain Layout
+
+fix
+\end_layout
+
+\end_inset
+
+, we get a simplified formula for 
+\begin_inset Formula $f$
+\end_inset
+
+:
+\begin_inset Formula 
+\begin{align*}
+ & f=u^{:F^{T}}\rightarrow s\triangleright(u\triangleright\text{fix})^{B}\\
+ & =u^{:F^{T}}\rightarrow u\triangleright(q^{:\forall X.\,(F^{X}\rightarrow X)\rightarrow X}\rightarrow s\triangleright q^{B})^{\uparrow F}\bef s\\
+ & =(q^{:\forall X.\,(F^{X}\rightarrow X)\rightarrow X}\rightarrow s\triangleright q^{B})^{\uparrow F}\bef s\quad.
+\end{align*}
+
+\end_inset
+
 It remains to verify that the assumption of the strong dinaturality law
  holds:
 \begin_inset Formula 
 \begin{align*}
  & r\bef f\overset{?}{=}f^{\uparrow F}\bef s\quad,\\
-\text{or equivalently}:\quad & \text{fix}^{\uparrow F}\bef(u\rightarrow s\triangleright(u\triangleright\text{fix}))\overset{?}{=}\big(u^{:F^{T}}\rightarrow s\triangleright(u\triangleright\text{fix})\big)^{\uparrow F}\bef s\quad.
+\text{or equivalently}:\quad & \text{fix}^{\uparrow F}\bef(q\rightarrow s\triangleright q^{B})^{\uparrow F}\bef s\overset{?}{=}f^{\uparrow F}\bef s\quad.
 \end{align*}
 
 \end_inset
 
+To prove the last equation, it is sufficient to prove that:
+\begin_inset Formula 
+\[
+\text{fix}\bef(q\rightarrow s\triangleright q^{B})=f\quad.
+\]
+
+\end_inset
+
 Rewrite the left-hand side above until it becomes equal to the right-hand
  side:
 \begin_inset Formula 
+\begin{align*}
+ & \text{fix}\bef(q\rightarrow s\triangleright q^{B})\\
+ & =(u^{:F^{T}}\rightarrow u\triangleright\text{fix})\bef(q\rightarrow s\triangleright q^{B})\\
+ & =u^{:F^{T}}\rightarrow s\triangleright(u\triangleright\text{fix})^{B}=f.
+\end{align*}
+
+\end_inset
+
+
+\begin_inset Note Note
+status collapsed
+
+\begin_layout Plain Layout
+\begin_inset Formula 
 \begin{align*}
  & \text{fix}^{\uparrow F}\bef(u\rightarrow s\triangleright(u\triangleright\text{fix}))=(u^{:F^{F^{T}}}\rightarrow u\triangleright\text{fix}^{\uparrow F})\bef(u\rightarrow s\triangleright(u\triangleright\text{fix}))\\
 \text{compute composition}:\quad & =u\rightarrow s\triangleright(u\triangleright\text{fix}^{\uparrow F}\triangleright\gunderline{\text{fix}})=\gunderline{u\rightarrow u\,\triangleright}\,\text{fix}^{\uparrow F}\triangleright(q\rightarrow s\triangleright q)^{\uparrow F}\bef s\\
@@ -35686,6 +35729,11 @@ Rewrite the left-hand side above until it becomes equal to the right-hand
 
 \end_inset
 
+
+\end_layout
+
+\end_inset
+
 The two sides are now equal.
 
 \begin_inset Formula $\square$

sofp-src/lyx/sofp-transformers.lyx

@@ -586,9 +586,8 @@ n[Int]] everywhere.
 
 \end_inset
 
-The type constructor forces us to use pattern matching with nested functor
- blocks, since that is the only way of getting access to values of type
-
+We are forced to use pattern matching with nested functor blocks, since
+ that is the only way of getting access to values of type 
 \begin_inset listings
 inline true
 status open
@@ -2474,31 +2473,31 @@ Solution
 \end_layout
 
 \begin_layout Standard
-There is no lawful 
+The type constructor 
 \begin_inset listings
 inline true
 status open
 
 \begin_layout Plain Layout
 
-flatMap
+Option[State[S, A]]
 \end_layout
 
 \end_inset
 
- function for the type constructor 
+ has no lawful 
 \begin_inset listings
 inline true
 status open
 
 \begin_layout Plain Layout
 
-Option[State[S, A]]
+flatMap
 \end_layout
 
 \end_inset
 
-:
+ function:
 \begin_inset listings
 inline false
 status open
@@ -4561,7 +4560,7 @@ noprefix "false"
 \end_layout
 
 \begin_layout Standard
-The type constructors for monad transformers are conventionally named 
+The type constructors for monad transformers are usually named as 
 \begin_inset listings
 inline true
 status open
@@ -4733,8 +4732,8 @@ implicit class ReaderTBaseLift[M[_]: Monad : Functor, R, A](t: R => A) {
 The lifts are written in the code notation as:
 \begin_inset Formula 
 \begin{align*}
-\text{foreign lift}:\quad & \text{flift}:M^{A}\rightarrow T_{\text{Reader}}^{M,A}\quad, & \text{flift}\,(m^{:M^{A}})\triangleq\_^{:R}\rightarrow m=\text{pu}_{\text{Reader}}(m)\quad,\quad~\\
-\text{base lift}:\quad & \text{blift}:(R\rightarrow A)\rightarrow T_{\text{Reader}}^{M,A}\quad, & \text{blift}\,(t^{:R\rightarrow A})\triangleq r^{:R}\rightarrow\text{pu}_{M}(t(r))=t\bef\text{pu}_{M}\quad.
+\text{foreign lift}:\quad & \text{flift}:M^{A}\rightarrow T_{\text{Reader}}^{M,A}\quad,\quad\quad\text{flift}\,(m^{:M^{A}})\triangleq\_^{:R}\rightarrow m=\text{pu}_{\text{Reader}}(m)\quad,\\
+\text{base lift}:\quad & \text{blift}:(R\rightarrow A)\rightarrow T_{\text{Reader}}^{M,A}\quad,\quad\quad\text{blift}\,(t^{:R\rightarrow A})\triangleq t\bef\text{pu}_{M}\quad.
 \end{align*}
 
 \end_inset
@@ -5154,10 +5153,11 @@ Writer
 's flatten methods:
 \begin_inset Formula 
 \begin{align*}
-\text{ftn}_{T}\big(t^{:M^{M^{A\times W}\times W}}\big) & =t\triangleright(m^{:M^{A\times W}}\times w^{:W}\rightarrow m\triangleright(p^{:A\times W}\rightarrow p\times w)^{\uparrow M})^{\uparrow M}\triangleright\text{ftn}_{M}\triangleright(\text{ftn}_{\text{Writer}})^{\uparrow M}\quad,\\
-\text{ftn}_{T} & =(m^{:M^{A\times W}}\times w^{:W}\rightarrow m\triangleright(p^{:A\times W}\rightarrow p\times w)^{\uparrow M})^{\uparrow M}\bef\text{ftn}_{M}\bef(\text{ftn}_{\text{Writer}})^{\uparrow M}\\
- & =\text{flm}_{M}(m\times w\rightarrow m\triangleright(p\rightarrow p\times w)^{\uparrow M}\bef\text{ftn}_{\text{Writer}}^{\uparrow M})\\
- & =\text{flm}_{M}(m\times w\rightarrow m\triangleright(a\times w_{2}\rightarrow a\times(w\oplus w_{2})))\quad.
+ & \text{ftn}_{T}\big(t^{:M^{M^{A\times W}\times W}}\big)\\
+ & \quad=t\triangleright(m^{:M^{A\times W}}\times w^{:W}\rightarrow m\triangleright(p^{:A\times W}\rightarrow p\times w)^{\uparrow M})^{\uparrow M}\triangleright\text{ftn}_{M}\triangleright(\text{ftn}_{\text{Writer}})^{\uparrow M}\quad,\\
+ & \text{ftn}_{T}=(m^{:M^{A\times W}}\times w^{:W}\rightarrow m\triangleright(p^{:A\times W}\rightarrow p\times w)^{\uparrow M})^{\uparrow M}\bef\text{ftn}_{M}\bef(\text{ftn}_{\text{Writer}})^{\uparrow M}\\
+ & \quad=\text{flm}_{M}(m\times w\rightarrow m\triangleright(p\rightarrow p\times w)^{\uparrow M}\bef\text{ftn}_{\text{Writer}}^{\uparrow M})\\
+ & \quad=\text{flm}_{M}(m\times w\rightarrow m\triangleright(a\times w_{2}\rightarrow a\times(w\oplus w_{2})))\quad.
 \end{align*}
 
 \end_inset

sofp-src/tex/sofp.tex

@@ -321,8 +321,8 @@
 {\footnotesize{}ISBN: 978-0-359-76877-6}\\
 \\
 {\scriptsize{}Source hash (sha256): cbd327cf5baeac2e9d58471a6d010dc2c542ea70d4d5c5a4c4c8ce793c5a5b43}\\
-{\scriptsize{}Git commit: 195c1f1251605e0eba92ac033f93ee2d0acaf5ef}\\
-{\scriptsize{}PDF file built on Sat, 04 May 2024 21:11:14 +0200 by pdfTeX 3.141592653-2.6-1.40.25 (TeX Live 2023) on Darwin}\\
+{\scriptsize{}Git commit: 35ba0d9120711fb25927dc04d722f92824b93408}\\
+{\scriptsize{}PDF file built on Sat, 04 May 2024 21:18:10 +0200 by pdfTeX 3.141592653-2.6-1.40.25 (TeX Live 2023) on Darwin}\\
 ~\\
 {\scriptsize{}Permission is granted to copy, distribute and/or modify
 this document under the terms of the GNU Free Documentation License,