stop using titlesec package

.github/workflows/build-pdf.yml

@@ -36,7 +36,7 @@ jobs:
         id: upload-pdf
         uses: actions/upload-artifact@v2
         with:
-          name: PDF files
+          name: PDF files and LaTeX logs
           path: |
             ./sofp-src/sofp*.pdf
             ./sofp-src/sofp-logs.tar.bz2

sofp-src/excluded_words

@@ -278,6 +278,7 @@
 ^cYD$
 ^cadabra$
 ^cadalgebra$
+^catamorphism$
 ^catsMonoidRoute$
 ^cb
 ^ccc$
@@ -442,6 +443,7 @@
 ^indices$
 ^inequivalent$
 ^init$
+^injective$
 ^inlined$
 ^intValue$
 ^intuitionistic$

sofp-src/sofp-free-type.lyx

@@ -10105,7 +10105,16 @@ larger
 \begin_inset Formula $L^{A}$
 \end_inset
 
- (lists and streams).
+ that includes both finite and infinite lists.
+ It is clear that 
+\begin_inset Formula $f_{1}$
+\end_inset
+
+ is injective; the same holds also for 
+\begin_inset Formula $f_{2}$
+\end_inset
+
+.
 \end_layout
 
 \begin_layout Standard
@@ -11337,11 +11346,27 @@ The Church encoding
 \begin_inset Formula $R$
 \end_inset
 
-, there is a unique fixpoint-preserving function 
+, there is a unique fixpoint-preserving map 
 \begin_inset Formula $T\rightarrow R$
 \end_inset
 
-.
+ called a catamorphism.
+ To define that map, assume that the fixpoint 
+\begin_inset Formula $R$
+\end_inset
+
+ has a known function 
+\begin_inset Formula $\text{fix}_{R}:F^{R}\rightarrow R$
+\end_inset
+
+ and write
+\begin_inset Formula 
+\[
+\text{cata}:T\rightarrow R\quad,\quad\quad\text{cata}\triangleq t^{:\forall X.\,(F^{X}\rightarrow X)\rightarrow X}\rightarrow\text{fix}_{R}\triangleright t^{R}\quad.
+\]
+
+\end_inset
+
  ***
 \end_layout
 

sofp-src/sofp-free-type.tex

@@ -2186,7 +2186,9 @@ \subsection{Recursive type equations with different fixpoints}
 and $L_{\text{inf}}^{A}$. To see this formally, we consider the functions
 $f_{1}:L_{\text{fin}}^{A}\rightarrow L^{A}$ and $f_{2}:L_{\text{inf}}^{A}\rightarrow L^{A}$.
 The function $f_{1}$ embeds values of type $L_{\text{fin}}^{A}$
-(finite lists) in the type $L^{A}$ (lists and streams).
+(finite lists) in the type $L^{A}$ that includes both finite and
+infinite lists. It is clear that $f_{1}$ is injective; the same holds
+also for $f_{2}$.
 
 Additionally, we can show that the functions $f_{1}$ and $f_{2}$
 preserve the fixpoint structure of the types. {*}{*}{*}
@@ -2440,8 +2442,13 @@ \subsubsection{Statement \label{subsec:Statement-strong-dinaturality-property-of
 
 The Church encoding $T\triangleq\forall X.\,(F^{X}\rightarrow X)\rightarrow X$
 of the fixpoint has a special property: for any other fixpoint $R$,
-there is a unique fixpoint-preserving function $T\rightarrow R$.
-{*}{*}{*}
+there is a unique fixpoint-preserving map $T\rightarrow R$ called
+a catamorphism. To define that map, assume that the fixpoint $R$
+has a known function $\text{fix}_{R}:F^{R}\rightarrow R$ and write
+\[
+\text{cata}:T\rightarrow R\quad,\quad\quad\text{cata}\triangleq t^{:\forall X.\,(F^{X}\rightarrow X)\rightarrow X}\rightarrow\text{fix}_{R}\triangleright t^{R}\quad.
+\]
+ {*}{*}{*}
 
 \subsection{The co-Yoneda identities}
 

sofp-src/sofp-monads.lyx

@@ -22053,20 +22053,10 @@ status open
 
 \begin_layout Plain Layout
 typeclass!
-\begin_inset listings
-inline true
-status open
-
-\begin_layout Plain Layout
-
+\family typewriter
 Monad
 \end_layout
 
-\end_inset
-
-
-\end_layout
-
 \end_inset
 
  for monads and a law-checking test function can be defined by

sofp-src/sofp-monads.tex

@@ -5048,7 +5048,7 @@ \subsection{From semimonads to monads: Motivation for the identity laws}
 {\color{greenunder}\text{right identity law of }M:}\quad & \text{flm}_{M}(\text{pu}_{M})=\text{id}^{:M^{A}\rightarrow M^{A}}\quad.\label{eq:monad-right-identity-law-for-flatMap}
 \end{align}
 
-A typeclass\index{typeclass!Monad@\lstinline!Monad!} for monads and
+A typeclass\index{typeclass!Monad@\texttt{Monad}} for monads and
 a law-checking test function can be defined by
 \begin{lstlisting}
 abstract class Monad[F[_]: Functor : Semimonad] {

sofp-src/sofp.lyx

@@ -17,14 +17,35 @@
 \usepackage{pstricks}
 
 % Fix the numbering of exercises: subsubsections appear as paragraphs but are numbered.
-\usepackage{titlesec}
+%\usepackage{titlesec} % Incompatible with komascript's later versions?
 % See https://tex.stackexchange.com/questions/7627/how-to-reference-paragraph
 % See the `titlesec` package documentation at http://www.ctex.org/documents/packages/layout/titlesec.pdf
-\titleformat{\subsubsection}[runin]{\normalfont\normalsize\bfseries}{}{0pt}{}
-\titlespacing{\subsubsection}{0pt}{5pt}{3\wordsep}
-\titleformat{\subparagraph}[runin]{\normalfont\normalsize\bfseries}{}{0pt}{}
-\titlespacing{\subparagraph}{\parindent}{\parskip}{3\wordsep}
-\titlespacing{\paragraph}{0pt}{3pt}{2\wordsep}
+%\titleformat{\subsubsection}[runin]{\normalfont\normalsize\bfseries}{}{0pt}{}
+%\titlespacing{\subsubsection}{0pt}{5pt}{3\wordsep}
+%\titleformat{\subparagraph}[runin]{\normalfont\normalsize\bfseries}{}{0pt}{}
+%\titlespacing{\subparagraph}{\parindent}{\parskip}{3\wordsep}
+%\titlespacing{\paragraph}{0pt}{3pt}{2\wordsep}
+
+\renewcommand*{\subsubsectionformat}{}
+\RedeclareSectionCommand[ % Statement 1.2.3.4
+  runin=true,
+  afterskip=2ex,
+  beforeskip=2.5pt plus 0.3pt minus 0.05pt,
+  afterindent=false,
+  font={\normalfont\normalsize\bfseries}
+]{subsubsection}
+\RedeclareSectionCommand[ % Proof
+  runin=true,
+  font={\normalfont\normalsize\bfseries},
+  afterindent=false,
+  afterskip=2ex,
+  beforeskip=0pt
+]{subparagraph}
+\RedeclareSectionCommand[
+  runin=true,
+  afterskip=1.3ex,
+  beforeskip=0pt
+]{paragraph}
 
 % Make page headers and page numbers smaller
 \addtokomafont{pagehead}{\small}

sofp-src/sofp.tex

@@ -74,14 +74,35 @@
 \usepackage{pstricks}
 
 % Fix the numbering of exercises: subsubsections appear as paragraphs but are numbered.
-\usepackage{titlesec}
+%\usepackage{titlesec} % Incompatible with komascript\textsf{'}s later versions?
 % See https://tex.stackexchange.com/questions/7627/how-to-reference-paragraph
 % See the `titlesec` package documentation at http://www.ctex.org/documents/packages/layout/titlesec.pdf
-\titleformat{\subsubsection}[runin]{\normalfont\normalsize\bfseries}{}{0pt}{}
-\titlespacing{\subsubsection}{0pt}{5pt}{3\wordsep}
-\titleformat{\subparagraph}[runin]{\normalfont\normalsize\bfseries}{}{0pt}{}
-\titlespacing{\subparagraph}{\parindent}{\parskip}{3\wordsep}
-\titlespacing{\paragraph}{0pt}{3pt}{2\wordsep}
+%\titleformat{\subsubsection}[runin]{\normalfont\normalsize\bfseries}{}{0pt}{}
+%\titlespacing{\subsubsection}{0pt}{5pt}{3\wordsep}
+%\titleformat{\subparagraph}[runin]{\normalfont\normalsize\bfseries}{}{0pt}{}
+%\titlespacing{\subparagraph}{\parindent}{\parskip}{3\wordsep}
+%\titlespacing{\paragraph}{0pt}{3pt}{2\wordsep}
+
+\renewcommand*{\subsubsectionformat}{}
+\RedeclareSectionCommand[ % Statement 1.2.3.4
+  runin=true,
+  afterskip=2ex,
+  beforeskip=2.5pt plus 0.3pt minus 0.05pt,
+  afterindent=false,
+  font={\normalfont\normalsize\bfseries}
+]{subsubsection}
+\RedeclareSectionCommand[ % Proof
+  runin=true,
+  font={\normalfont\normalsize\bfseries},
+  afterindent=false,
+  afterskip=2ex,
+  beforeskip=0pt
+]{subparagraph}
+\RedeclareSectionCommand[
+  runin=true,
+  afterskip=1.3ex,
+  beforeskip=0pt
+]{paragraph}
 
 % Make page headers and page numbers smaller
 \addtokomafont{pagehead}{\small}
@@ -248,8 +269,8 @@
 ~\\
 ISBN: 978-0-359-76877-6\\
 \\
-{\scriptsize{}Source hash: ec23f32797ba47ca13bd6dbfd8952ef0a7ae2d565668d617ab01e3fe217c99ee}\\
-{\scriptsize{}Git commit: bdc9913567921e2a90d2444af520ffa92fa12d42}\\
+{\scriptsize{}Source hash: 3515c69cb444b87f936718c788552de2c08f6770282e8efc9ac274deecac4799}\\
+{\scriptsize{}Git commit: c1f1b28b34ff90d02ac51ba7313a0234de2b46be}\\
 ~\\
 {\scriptsize{}Permission is granted to copy, distribute and/or modify
 this document under the terms of the GNU Free Documentation License,