diff --git a/ctfp.pdf b/ctfp.pdf
index 6a3abc8..f926dda 100644
Binary files a/ctfp.pdf and b/ctfp.pdf differ
diff --git a/src/content/1.1/Category - The Essence of Composition.tex b/src/content/1.1/Category - The Essence of Composition.tex
index b5bab08..9eb2700 100644
--- a/src/content/1.1/Category - The Essence of Composition.tex	
+++ b/src/content/1.1/Category - The Essence of Composition.tex	
@@ -16,7 +16,7 @@ object B to object C, then there must be an arrow --- their composition
 \caption{In a category, if there is an arrow going from A to B and an arrow going from B to C then there must also be a direct arrow from A to C that is their composition. This diagram is not a full category because it’s missing identity morphisms (see later).}
 \end{figure}
 
-\subsection{Arrows as Functions}\label{arrows-as-functions}
+\section{Arrows as Functions}\label{arrows-as-functions}
 
 Is this already too much abstract nonsense? Do not despair. Let's talk
 concretes. Think of arrows, which are also called \newterm{morphisms}, as
@@ -96,7 +96,7 @@ of\ldots{}'' A function type is created by inserting an arrow between
 two types. You compose two functions by inserting a period between them
 (or a Unicode circle).
 
-\subsection{Properties of Composition}\label{properties-of-composition}
+\section{Properties of Composition}\label{properties-of-composition}
 
 There are two extremely important properties that the composition in any
 category must satisfy.
@@ -203,7 +203,7 @@ To summarize: A category consists of objects and arrows (morphisms).
 Arrows can be composed, and the composition is associative. Every object
 has an identity arrow that serves as a unit under composition.
 
-\subsection{Composition is the Essence of
+\section{Composition is the Essence of
 Programming}\label{composition-is-the-essence-of-programming}
 
 Functional programmers have a peculiar way of approaching problems. They
@@ -268,7 +268,7 @@ you have to dig into the implementation of the object in order to
 understand how to compose it with other objects, you've lost the
 advantages of your programming paradigm.
 
-\subsection{Challenges}\label{challenges}
+\section{Challenges}\label{challenges}
 
 \begin{enumerate}
 \tightlist
diff --git a/src/content/1.10/Natural Transformations.tex b/src/content/1.10/Natural Transformations.tex
index 9d52d88..28a2aaf 100644
--- a/src/content/1.10/Natural Transformations.tex	
+++ b/src/content/1.10/Natural Transformations.tex	
@@ -125,7 +125,7 @@ like saying they are the same. \newterm{Natural isomorphism} is defined as
 a natural transformation whose components are all isomorphisms
 (invertible morphisms).
 
-\subsection{Polymorphic Functions}\label{polymorphic-functions}
+\section{Polymorphic Functions}\label{polymorphic-functions}
 
 We talked about the role of functors (or, more specifically,
 endofunctors) in programming. They correspond to type constructors that
@@ -391,7 +391,7 @@ two elements of the \code{Maybe\ ()} type, which are \code{Nothing}
 and \code{Just\ ()}. We'll come back to the Yoneda lemma later ---
 this was just a little teaser.
 
-\subsection{Beyond Naturality}\label{beyond-naturality}
+\section{Beyond Naturality}\label{beyond-naturality}
 
 A parametrically polymorphic function between two functors (including
 the edge case of the \code{Const} functor) is always a natural
@@ -467,7 +467,7 @@ transformation. Interestingly, there is a generalization of natural
 transformations, called dinatural transformations, that deals with such
 cases. We'll get to them when we discuss ends.
 
-\subsection{Functor Category}\label{functor-category}
+\section{Functor Category}\label{functor-category}
 
 Now that we have mappings between functors --- natural transformations
 --- it's only natural to ask the question whether functors form a
@@ -586,7 +586,7 @@ And by ``object'' in \textbf{Cat} I mean a category, so
 D\textsuperscript{C} is a category, which we can identify with the
 functor category between C and D.
 
-\subsection{2-Categories}\label{categories}
+\section{2-Categories}\label{categories}
 
 With that out of the way, let's have a closer look at \textbf{Cat}. By
 definition, any Hom-set in \textbf{Cat} is a set of functors. But, as we
@@ -779,7 +779,7 @@ Similarly:
 
 is a horizontal composition of α after 1\textsubscript{F}.
 
-\subsection{Conclusion}\label{conclusion}
+\section{Conclusion}\label{conclusion}
 
 This concludes the first part of the book. We've learned the basic
 vocabulary of category theory. You may think of objects and categories
@@ -805,7 +805,7 @@ Functors may be looked upon as objects in the functor category. As such,
 they become sources and targets of morphisms: natural transformations. A
 natural transformation is a special type of polymorphic function.
 
-\subsection{Challenges}\label{challenges}
+\section{Challenges}\label{challenges}
 
 \begin{enumerate}
 \item
@@ -847,7 +847,7 @@ Next:
 \href{https://bartoszmilewski.com/2015/04/15/category-theory-and-declarative-programming/}{Declarative
 Programming}.
 
-\subsection{Acknowledgments}\label{acknowledgments}
+\section{Acknowledgments}\label{acknowledgments}
 
 I'd like to thank Gershom Bazerman for checking my math and logic, and
 André van Meulebrouck, who has been volunteering his editing help.\\
diff --git a/src/content/1.2/Types and Functions.tex b/src/content/1.2/Types and Functions.tex
index ddf8706..4747442 100644
--- a/src/content/1.2/Types and Functions.tex	
+++ b/src/content/1.2/Types and Functions.tex	
@@ -1,7 +1,7 @@
 \lettrine[lhang=0.17]{T}{he category of types and functions} plays an important role in
 programming, so let's talk about what types are and why we need them.
 
-\subsection{Who Needs Types?}\label{who-needs-types}
+\section{Who Needs Types?}\label{who-needs-types}
 
 There seems to be some controversy about the advantages of static vs.
 dynamic and strong vs. weak typing. Let me illustrate these choices with
@@ -35,7 +35,7 @@ The analog of a type checker would go even further by making sure that,
 once Romeo is declared a human being, he doesn't sprout leaves or trap
 photons in his powerful gravitational field.
 
-\subsection{Types Are About
+\section{Types Are About
 Composability}\label{types-are-about-composability}
 
 Category theory is about composing arrows. But not any two arrows can be
@@ -95,7 +95,7 @@ sites. Unit testing may catch some of the mismatches, but testing is
 almost always a probabilistic rather than a deterministic process.
 Testing is a poor substitute for proof.
 
-\subsection{What Are Types?}\label{what-are-types}
+\section{What Are Types?}\label{what-are-types}
 
 The simplest intuition for types is that they are sets of values. The
 type \code{Bool} (remember, concrete types start with a capital letter
@@ -189,7 +189,7 @@ okay to ignore non-terminating functions and bottoms, and treat
 John Hughes, Patrik Jansson, Jeremy Gibbons, \href{http://www.cs.ox.ac.uk/jeremy.gibbons/publications/fast+loose.pdf}{
 Fast and Loose Reasoning is Morally Correct}. This paper provides justification for ignoring bottoms in most contexts.}
 
-\subsection{Why Do We Need a Mathematical
+\section{Why Do We Need a Mathematical
 Model?}\label{why-do-we-need-a-mathematical-model}
 
 As a programmer you are intimately familiar with the syntax and grammar
@@ -239,14 +239,15 @@ usually quite simple, if not trivial.
 Consider the definition of a factorial function in Haskell, which is a
 language quite amenable to denotational semantics:
 
-\mint{haskell}|fact n = product [1..n]|
-
+\begin{verbatim}
+fact n = product [1..n]
+\end{verbatim}
 The expression \code{{[}1..n{]}} is a list of integers from \code{1} to \code{n}.
 The function \code{product} multiplies all elements of a list. That's
 just like a definition of factorial taken from a math text. Compare this
 with C:
 
-\begin{minted}{c}
+\begin{verbatim}
 int fact(int n) {
     int i;
     int result = 1;
@@ -254,8 +255,7 @@ int fact(int n) {
         result *= i;
     return result;
 }
-\end{minted}
-
+\end{verbatim}
 Need I say more?
 
 Okay, I'll be the first to admit that this was a cheap shot! A factorial
@@ -283,7 +283,7 @@ even when writing web applications for the health system, you may
 appreciate the thought that functions and algorithms from the Haskell
 standard library come with proofs of correctness.
 
-\subsection{Pure and Dirty Functions}\label{pure-and-dirty-functions}
+\section{Pure and Dirty Functions}\label{pure-and-dirty-functions}
 
 The things we call functions in C++ or any other imperative language,
 are not the same things mathematicians call functions. A mathematical
@@ -311,7 +311,7 @@ about side effects separately. Later we'll see how monads let us model
 all kinds of effects using only pure functions. So we really don't lose
 anything by restricting ourselves to mathematical functions.
 
-\subsection{Examples of Types}\label{examples-of-types}
+\section{Examples of Types}\label{examples-of-types}
 
 Once you realize that types are sets, you can think of some rather
 exotic types. For instance, what's the type corresponding to an empty
@@ -325,8 +325,9 @@ return, there are no restrictions whatsoever. It can return any type
 it's a function that's polymorphic in the return type. Haskellers have a
 name for it:
 
-\mint{haskell}|absurd :: Void -> a|
-
+\begin{verbatim}
+absurd :: Void -> a
+\end{verbatim}
 (Remember, \code{a} is a type variable that can stand for any type.)
 The name is not coincidental. There is deeper interpretation of types
 and functions in terms of logic called the Curry-Howard isomorphism. The
@@ -341,8 +342,9 @@ Think of functions from and to this type. A function from \code{void}
 can always be called. If it's a pure function, it will always return the
 same result. Here's an example of such a function:
 
-\mint{c}|int f44() { return 44; }|
-
+\begin{verbatim}
+int f44() { return 44; }
+\end{verbatim}
 You might think of this function as taking ``nothing'', but as we've
 just seen, a function that takes ``nothing'' can never be called because
 there is no value representing ``nothing.'' So what does this function
@@ -355,19 +357,19 @@ because of the Haskell's love of terseness, the same symbol \code{()}
 is used for the type, the constructor, and the only value corresponding
 to a singleton set. So here's this function in Haskell:
 
-\begin{minted}{haskell}
+\begin{verbatim}
 f44 :: () -> Integer
 f44 () = 44
-\end{minted}
-
+\end{verbatim}
 The first line declares that \code{f44} takes the type \code{()},
 pronounced ``unit,'' into the type \code{Integer}. The second line
 defines \code{f44} by pattern matching the only constructor for unit,
 namely \code{()}, and producing the number 44. You call this function
 by providing the unit value \code{()}:
 
-\mint{haskell}|f44 ()|
-
+\begin{verbatim}
+f44 ()
+\end{verbatim}
 Notice that every function of unit is equivalent to picking a single
 element from the target type (here, picking the \code{Integer} 44). In
 fact you could think of \code{f44} as a different representation for
@@ -387,21 +389,19 @@ element of A to the single element of that singleton set. For every A
 there is exactly one such function. Here's this function for
 \code{Integer}:
 
-\begin{minted}{haskell}
+\begin{verbatim}
 fInt :: Integer -> ()
 fInt x = ()
-\end{minted}
-
+\end{verbatim}
 You give it any integer, and it gives you back a unit. In the spirit of
 terseness, Haskell lets you use the wildcard pattern, the underscore,
 for an argument that is discarded. This way you don't have to invent a
 name for it. So the above can be rewritten as:
 
-\begin{minted}{haskell}
+\begin{verbatim}
 fInt :: Integer -> ()
 fInt _ = ()
-\end{minted}
-
+\end{verbatim}
 Notice that the implementation of this function not only doesn't depend
 on the value passed to it, but it doesn't even depend on the type of the
 argument.
@@ -412,38 +412,34 @@ such functions with one equation using a type parameter instead of a
 concrete type. What should we call a polymorphic function from any type
 to unit type? Of course we'll call it \code{unit}:
 
-\begin{minted}{haskell}
+\begin{verbatim}
 unit :: a -> ()
 unit _ = ()
-\end{minted}
-
+\end{verbatim}
 In C++ you would write this function as:
 
-\begin{minted}{c++}
+\begin{verbatim}
 template<class T>
 void unit(T) {}
-\end{minted}
-
+\end{verbatim}
 Next in the typology of types is a two-element set. In C++ it's called
 \code{bool} and in Haskell, predictably, \code{Bool}. The difference
 is that in C++ \code{bool} is a built-in type, whereas in Haskell it
 can be defined as follows:
 
-\begin{minted}{haskell}
+\begin{verbatim}
 data Bool = True | False
-\end{minted}
-
+\end{verbatim}
 (The way to read this definition is that \code{Bool} is either
 \code{True} or \code{False}.) In principle, one should also be able
 to define a Boolean type in C++ as an enumeration:
 
-\begin{minted}{c++}
+\begin{verbatim}
 enum bool { 
     true,
     false
 };
-\end{minted}
-
+\end{verbatim}
 but C++ \code{enum} is secretly an integer. The C++11
 ``\code{enum class}'' could have been used instead, but then you
 would have to qualify its values with the class name, as in
@@ -462,7 +458,7 @@ Boolean. The actual predicates are defined in \code{std::ctype} and
 have the form \code{ctype::is(alpha,\ c)},
 \code{ctype::is(digit,\ c)}, etc.
 
-\subsection{Challenges}\label{challenges}
+\section{Challenges}\label{challenges}
 
 \begin{enumerate}
 \tightlist
@@ -495,25 +491,25 @@ have the form \code{ctype::is(alpha,\ c)},
   \item
     The factorial function from the example in the text.
   \item
-\begin{minted}{c++}
+\begin{verbatim}
 std::getchar()
-\end{minted}
+\end{verbatim}
   \item
-\begin{minted}{c++}
+\begin{verbatim}
 bool f() { 
     std::cout << "Hello!" << std::endl;
     return true;
 }
-\end{minted}
+\end{verbatim}
   \item
-\begin{minted}{c++}
+\begin{verbatim}
 int f(int x)
 {
     static int y = 0;
     y += x;
     return y;
 }
-\end{minted}
+\end{verbatim}
   \end{enumerate}
 \item
   How many different functions are there from \code{Bool} to
diff --git a/src/content/1.3/Categories Great and Small.tex b/src/content/1.3/Categories Great and Small.tex
index c1762f1..d390a1d 100644
--- a/src/content/1.3/Categories Great and Small.tex	
+++ b/src/content/1.3/Categories Great and Small.tex	
@@ -2,7 +2,7 @@
 examples. Categories come in all shapes and sizes and often pop up in
 unexpected places. We'll start with something really simple.
 
-\subsection{No Objects}\label{no-objects}
+\section{No Objects}\label{no-objects}
 
 The most trivial category is one with zero objects and, consequently,
 zero morphisms. It's a very sad category by itself, but it may be
@@ -10,7 +10,7 @@ important in the context of other categories, for instance, in the
 category of all categories (yes, there is one). If you think that an
 empty set makes sense, then why not an empty category?
 
-\subsection{Simple Graphs}\label{simple-graphs}
+\section{Simple Graphs}\label{simple-graphs}
 
 You can build categories just by connecting objects with arrows. You can
 imagine starting with any directed graph and making it into a category
@@ -34,7 +34,7 @@ given structure by extending it with a minimum number of items to
 satisfy its laws (here, the laws of a category). We'll see more examples
 of it in the future.
 
-\subsection{Orders}\label{orders}
+\section{Orders}\label{orders}
 
 And now for something completely different! A category where a morphism
 is a relation between objects: the relation of being less than or equal.
@@ -71,7 +71,7 @@ and total orders because of sorting. Sorting algorithms, such as
 quicksort, bubble sort, merge sort, etc., can only work correctly on
 total orders. Partial orders can be sorted using topological sort.
 
-\subsection{Monoid as Set}\label{monoid-as-set}
+\section{Monoid as Set}\label{monoid-as-set}
 
 Monoid is an embarrassingly simple but amazingly powerful concept. It's
 the concept behind basic arithmetics: Both addition and multiplication
@@ -243,7 +243,7 @@ std::string mappend(std::string s1, std::string s2) {
 }
 \end{minted}
 
-\subsection{Monoid as Category}\label{monoid-as-category}
+\section{Monoid as Category}\label{monoid-as-category}
 
 That was the ``familiar'' definition of the monoid in terms of elements
 of a set. But as you know, in category theory we try to get away from
@@ -333,12 +333,12 @@ follow the rules of composition, and as points in a set. Here,
 composition of morphisms in M translates into monoidal product in the
 set \code{M(m, m)}.
 
-\subsection{Acknowledgments}\label{acknowledgments}
+\section{Acknowledgments}\label{acknowledgments}
 
 I'd like to thank Andrew Sutton for rewriting my C++ monoid concept code
 according to his and Bjarne Stroustrup's latest proposal.
 
-\subsection{Challenges}\label{challenges}
+\section{Challenges}\label{challenges}
 
 \begin{enumerate}
 \item
diff --git a/src/content/1.4/Kleisli Categories.tex b/src/content/1.4/Kleisli Categories.tex
index 30aeb9c..e5bc4f7 100644
--- a/src/content/1.4/Kleisli Categories.tex	
+++ b/src/content/1.4/Kleisli Categories.tex	
@@ -169,7 +169,7 @@ composition} itself. But composition is the essence of category theory,
 so before we write more code, let's analyze the problem from the
 categorical point of view.
 
-\subsection{The Writer Category}\label{the-writer-category}
+\section{The Writer Category}\label{the-writer-category}
 
 The idea of embellishing the return types of a bunch of functions in
 order to piggyback some additional functionality turns out to be very
@@ -319,7 +319,7 @@ writer should be able to identify the bare minimum of constraints that
 make the library work --- here the logging library's only requirement is
 that the log have monoidal properties.
 
-\subsection{Writer in Haskell}\label{writer-in-haskell}
+\section{Writer in Haskell}\label{writer-in-haskell}
 
 The same thing in Haskell is a little more terse, and we also get a lot
 more help from the compiler. Let's start by defining the \code{Writer}
@@ -420,7 +420,7 @@ process :: String -> Writer [String]
 process = upCase >=> toWords
 \end{minted}
 
-\subsection{Kleisli Categories}\label{kleisli-categories}
+\section{Kleisli Categories}\label{kleisli-categories}
 
 You might have guessed that I haven't invented this category on the
 spot. It's an example of the so called Kleisli category --- a category
@@ -449,7 +449,7 @@ freedom which makes it possible to give simple denotational semantics to
 programs that in imperative languages are traditionally implemented
 using side effects.
 
-\subsection{Challenge}\label{challenge}
+\section{Challenge}\label{challenge}
 
 A function that is not defined for all possible values of its argument
 is called a partial function. It's not really a function in the
@@ -496,7 +496,7 @@ Here's the challenge:
   whenever possible.
 \end{enumerate}
 
-\subsection{Acknowledgments}\label{acknowledgments}
+\section{Acknowledgments}\label{acknowledgments}
 
 I'm grateful to Eric Niebler for reading the draft and providing the
 clever implementation of \code{compose} that uses advanced features of
diff --git a/src/content/1.5/Products and Coproducts.tex b/src/content/1.5/Products and Coproducts.tex
index bd11883..072a426 100644
--- a/src/content/1.5/Products and Coproducts.tex	
+++ b/src/content/1.5/Products and Coproducts.tex	
@@ -21,7 +21,7 @@ hits, you refine your query. That increases its \emph{precision}.
 Finally, the search engine will rank the hits and, hopefully, the one
 result that you're interested in will be at the top of the list.
 
-\subsection{Initial Object}\label{initial-object}
+\section{Initial Object}\label{initial-object}
 
 The simplest shape is a single object. Obviously, there are as many
 instances of this shape as there are objects in a given category. That's
@@ -77,7 +77,7 @@ absurd :: Void -> a
 It's this family of morphisms that makes \code{Void} the initial
 object in the category of types.
 
-\subsection{Terminal Object}\label{terminal-object}
+\section{Terminal Object}\label{terminal-object}
 
 Let's continue with the single-object pattern, but let's change the way
 we rank the objects. We'll say that object \emph{a} is ``more terminal''
@@ -135,7 +135,7 @@ no _ = False
 Insisting on uniqueness gives us just the right precision to narrow down
 the definition of the terminal object to just one type.
 
-\subsection{Duality}\label{duality}
+\section{Duality}\label{duality}
 
 You can't help but to notice the symmetry between the way we defined the
 initial object and the terminal object. The only difference between the
@@ -163,7 +163,7 @@ the arrows twice gets us back to the original state.
 It follows then that a terminal object is the initial object in the
 opposite category.
 
-\subsection{Isomorphisms}\label{isomorphisms}
+\section{Isomorphisms}\label{isomorphisms}
 
 As programmers, we are well aware that defining equality is a nontrivial
 task. What does it mean for two objects to be equal? Do they have to
@@ -235,7 +235,7 @@ there could be more than one isomorphism between two objects, but that's
 not the case here. This ``uniqueness up to unique isomorphism'' is the
 important property of all universal constructions.
 
-\subsection{Products}\label{products}
+\section{Products}\label{products}
 
 The next universal construction is that of a product. We know what a
 cartesian product of two sets is: it's a set of pairs. But what's the
@@ -472,7 +472,7 @@ factorizer :: (c -> a) -> (c -> b) -> (c -> (a, b))
 factorizer p q = \x -> (p x, q x)
 \end{verbatim}
 
-\subsection{Coproduct}\label{coproduct}
+\section{Coproduct}\label{coproduct}
 
 Like every construction in category theory, the product has a dual,
 which is called the coproduct. When we reverse the arrows in the product
@@ -607,7 +607,7 @@ factorizer i j (Left a)  = i a
 factorizer i j (Right b) = j b
 \end{verbatim}
 
-\subsection{Asymmetry}\label{asymmetry}
+\section{Asymmetry}\label{asymmetry}
 
 We've seen two set of dual definitions: The definition of a terminal
 object can be obtained from the definition of the initial object by
@@ -704,7 +704,7 @@ collapsing. They are called \newterm{bijections} and they are truly
 symmetric, because they are invertible. In the category of sets, an
 isomorphism is the same as a bijection.
 
-\subsection{Challenges}\label{challenges}
+\section{Challenges}\label{challenges}
 
 \begin{enumerate}
   \tightlist
@@ -755,7 +755,7 @@ int j(bool b) { return b? 0: 1; }
   allows multiple acceptable morphisms from it to \code{Either}.
 \end{enumerate}
 
-\subsection{Bibliography}\label{bibliography}
+\section{Bibliography}\label{bibliography}
 
 \begin{enumerate}
 \tightlist
@@ -765,7 +765,7 @@ int j(bool b) { return b? 0: 1; }
   Coproducts} video.
 \end{enumerate}
 
-\subsection{Acknowledments}\label{acknowledments}
+\section{Acknowledments}\label{acknowledments}
 
 I'm grateful to Gershom Bazerman for reviewing this post before
 publication and for stimulating discussions.
\ No newline at end of file
diff --git a/src/content/1.6/Simple Algebraic Data Types.tex b/src/content/1.6/Simple Algebraic Data Types.tex
index 7d32ad1..eaf83e0 100644
--- a/src/content/1.6/Simple Algebraic Data Types.tex	
+++ b/src/content/1.6/Simple Algebraic Data Types.tex	
@@ -12,7 +12,7 @@ large subset of composite types.
 Let's have a closer look at product and sum types as they appear in
 programming.
 
-\subsection{Product Types}\label{product-types}
+\section{Product Types}\label{product-types}
 
 The canonical implementation of a product of two types in a programming
 language is a pair. In Haskell, a pair is a primitive type constructor;
@@ -192,7 +192,7 @@ and error prone --- keeping track of which component represents what.
 It's often preferable to give names to components. A product type with
 named fields is called a record in Haskell, and a \code{struct} in C.
 
-\subsection{Records}\label{records}
+\section{Records}\label{records}
 
 Let's have a look at a simple example. We want to describe chemical
 elements by combining two strings, name and symbol; and an integer, the
@@ -264,7 +264,7 @@ startsWithSymbol e = symbol e `isPrefixOf` name e
 The parentheses could be omitted in this case, because an infix operator
 has lower precedence than a function call.
 
-\subsection{Sum Types}\label{sum-types}
+\section{Sum Types}\label{sum-types}
 
 Just as the product in the category of sets gives rise to product types,
 the coproduct gives rise to sum types. The canonical implementation of a
@@ -457,7 +457,7 @@ You will rarely see \code{union} used as a sum type in C++ because of
 severe limitations on what can go into a union. You can't even put a
 \code{std::string} into a union because it has a copy constructor.
 
-\subsection{Algebra of Types}\label{algebra-of-types}
+\section{Algebra of Types}\label{algebra-of-types}
 
 Taken separately, product and sum types can be used to define a variety
 of useful data structures, but the real strength comes from combining
@@ -649,7 +649,7 @@ This analogy goes deeper, and is the basis of the Curry-Howard
 isomorphism between logic and type theory. We'll come back to it when we
 talk about function types.
 
-\subsection{Challenges}\label{challenges}
+\section{Challenges}\label{challenges}
 
 \begin{enumerate}
 \tightlist
@@ -700,7 +700,7 @@ circ (Rect d h) = 2.0 * (d + h)
   according to our translation table.
 \end{enumerate}
 
-\subsection{Acknowledments}\label{acknowledments}
+\section{Acknowledments}\label{acknowledments}
 
 Thanks go to Gershom Bazerman for reviewing this post and helpful
 comments.
diff --git a/src/content/1.7/Functors.tex b/src/content/1.7/Functors.tex
index 701f2ac..b1008d3 100644
--- a/src/content/1.7/Functors.tex
+++ b/src/content/1.7/Functors.tex
@@ -84,7 +84,7 @@ maps every morphism in the source category to the identity morphism
 everything into one singularity. We'll see more of this functor when we
 discuss limits and colimits.
 
-\subsection{Functors in Programming}\label{functors-in-programming}
+\section{Functors in Programming}\label{functors-in-programming}
 
 Let's get down to earth and talk about programming. We have our category
 of types and functions. We can talk about functors that map this
@@ -549,7 +549,7 @@ This combination of the type constructor \code{(-\textgreater{})\ r}
 with the above implementation of \code{fmap} is called the reader
 functor.
 
-\subsection{Functors as Containers}\label{functors-as-containers}
+\section{Functors as Containers}\label{functors-as-containers}
 
 We've seen some examples of functors in programming languages that
 define general-purpose containers, or at least objects that contain some
@@ -646,7 +646,7 @@ role in many constructions. In category theory, it's a special case of
 the Δ\textsubscript{c} functor I mentioned earlier --- the endo-functor
 case of a black hole. We'll be seeing more of it it in the future.
 
-\subsection{Functor Composition}\label{functor-composition}
+\section{Functor Composition}\label{functor-composition}
 
 It's not hard to convince yourself that functors between categories
 compose, just like functions between sets compose. A composition of two
@@ -739,7 +739,7 @@ these things because I find it pretty amazing that we can recognize the
 same structures repeating themselves at many levels of abstraction.
 We'll see later that functors form categories as well.
 
-\subsection{Challenges}\label{challenges}
+\section{Challenges}\label{challenges}
 
 \begin{enumerate}
 \item
@@ -762,7 +762,7 @@ fmap _ _ = Nothing
   words, use \newterm{induction}).
 \end{enumerate}
 
-\subsection{Acknowledgments}\label{acknowledgments}
+\section{Acknowledgments}\label{acknowledgments}
 
 Gershom Bazerman is kind enough to keep reviewing these posts. I'm
 grateful for his patience and insight.
diff --git a/src/content/1.8/Functoriality.tex b/src/content/1.8/Functoriality.tex
index 055a048..348aeb7 100644
--- a/src/content/1.8/Functoriality.tex
+++ b/src/content/1.8/Functoriality.tex
@@ -11,7 +11,7 @@ it's interesting to see which type constructors (which correspond to
 mappings between objects in a category) can be extended to functors
 (which include mappings between morphisms).
 
-\subsection{Bifunctors}\label{bifunctors}
+\section{Bifunctors}\label{bifunctors}
 
 Since functors are morphisms in \newterm{Cat} (the category of categories),
 a lot of intuitions about morphisms --- and functions in particular ---
@@ -107,7 +107,7 @@ and \code{second} and accepting the default for \code{bimap} (of
 course, you may implement all three of them, but then it's up to you to
 make sure they are related to each other in this manner).
 
-\subsection{Product and Coproduct
+\section{Product and Coproduct
 Bifunctors}\label{product-and-coproduct-bifunctors}
 
 An important example of a bifunctor is the categorical product --- a
@@ -162,7 +162,7 @@ morphisms. We are now one step closer to the full definition of a
 monoidal category (we still need to learn about naturality, before we
 can get there).
 
-\subsection{Functorial Algebraic Data
+\section{Functorial Algebraic Data
 Types}\label{functorial-algebraic-data-types}
 
 We've seen several examples of parameterized data types that turned out
@@ -327,7 +327,7 @@ own typeclasses, but that's a bit more advanced. The idea though is the
 same: You provide the behavior for the basic building blocks and sums
 and products, and let the compiler figure out the rest.
 
-\subsection{Functors in C++}\label{functors-in-c}
+\section{Functors in C++}\label{functors-in-c}
 
 If you are a C++ programmer, you obviously are on your own as far as
 implementing functors goes. However, you should be able to recognize
@@ -397,7 +397,7 @@ instance Functor Tree where fmap f (Leaf a) = Leaf (f a) fmap f (Node t t&apos;)
 
 This implementation can also be automatically derived by the compiler.
 
-\subsection{The Writer Functor}\label{the-writer-functor}
+\section{The Writer Functor}\label{the-writer-functor}
 
 I promised that I would come back to the
 \href{https://bartoszmilewski.com/2014/12/23/kleisli-categories/}{Kleisli
@@ -472,7 +472,7 @@ the way Haskell implements polymorphic functions. It's called
 an implementation of \code{fmap} for a given type constructor, one
 that preserves identity, then it must be unique.
 
-\subsection{Covariant and Contravariant
+\section{Covariant and Contravariant
 Functors}\label{covariant-and-contravariant-functors}
 
 Now that we've reviewed the writer functor, let's go back to the reader
@@ -591,7 +591,7 @@ With it, we get:
 contramap = flip (.)
 \end{verbatim}
 
-\subsection{Profunctors}\label{profunctors}
+\section{Profunctors}\label{profunctors}
 
 We've seen that the function-arrow operator is contravariant in its
 first argument and covariant in the second. Is there a name for such a
@@ -633,7 +633,7 @@ instance Profunctor (->) where dimap ab cd bc = cd . bc . ab lmap = flip (.) rma
 Profunctors have their application in the Haskell lens library. We'll
 see them again when we talk about ends and coends.
 
-\subsection{Challenges}\label{challenges}
+\section{Challenges}\label{challenges}
 
 \begin{enumerate}
 \item
@@ -704,7 +704,7 @@ Next:
 \href{https://bartoszmilewski.com/2015/03/13/function-types/}{Function
 Types}.
 
-\subsection{Acknowledgment}\label{acknowledgment}
+\section{Acknowledgment}\label{acknowledgment}
 
 As usual, big thanks go to Gershom Bazerman for reviewing this
 article.\\
diff --git a/src/content/1.9/Function Types.tex b/src/content/1.9/Function Types.tex
index 0bd1bca..c427e54 100644
--- a/src/content/1.9/Function Types.tex	
+++ b/src/content/1.9/Function Types.tex	
@@ -35,7 +35,7 @@ function types special. But there is a way, at least in some categories,
 to construct objects that represent hom-sets. Such objects are called
 \newterm{internal} hom-sets.
 
-\subsection{Universal Construction}\label{universal-construction}
+\section{Universal Construction}\label{universal-construction}
 
 Let's forget for a moment that function types are sets and try to
 construct a function type, or more generally, an internal hom-set, from
@@ -213,7 +213,7 @@ This is why, in Haskell, we interpret the function type
 \code{a-\textgreater{}b} as the categorical function object
 \code{a⇒b}.
 
-\subsection{Currying}\label{currying}
+\section{Currying}\label{currying}
 
 Let's have a second look at all the candidates for the function object.
 This time, however, let's think of the morphism \code{g} as a function
@@ -361,7 +361,7 @@ def catstr(s1: String)(s2: String) = s1 + s2
 Of course that requires some amount of foresight or prescience on the
 part of a library writer.
 
-\subsection{Exponentials}\label{exponentials}
+\section{Exponentials}\label{exponentials}
 
 In mathematical literature, the function object, or the internal
 hom-object between two objects \code{a} and \code{b}, is often
@@ -418,7 +418,7 @@ explains the identification of Haskell's function type with the
 categorical exponential object --- which corresponds more to our idea of
 \emph{data}.
 
-\subsection{Cartesian Closed
+\section{Cartesian Closed
 Categories}\label{cartesian-closed-categories}
 
 Although I will continue using the category of sets as a model for types
@@ -463,7 +463,7 @@ is called a \newterm{bicartesian closed} category. We'll see in the next
 section that bicartesian closed categories, of which \textbf{Set} is a
 prime example, have some interesting properties.
 
-\subsection{Exponentials and Algebraic Data
+\section{Exponentials and Algebraic Data
 Types}\label{exponentials-and-algebraic-data-types}
 
 The interpretation of function types as exponentials fits very well into
@@ -591,7 +591,7 @@ It's pretty incredible how those simple high-school algebraic identities
 can be lifted to category theory and have practical application in
 functional programming.
 
-\subsection{Curry-Howard Isomorphism}\label{curry-howard-isomorphism}
+\section{Curry-Howard Isomorphism}\label{curry-howard-isomorphism}
 
 I have already mentioned the correspondence between logic and algebraic
 data types. The \code{Void} type and the unit type \code{()}
@@ -716,7 +716,7 @@ coproducts, function types, and so on. And, as if to dispel any doubts,
 the theory is being formulated in Coq and Agda. Computers are
 revolutionizing the world in more than one way.
 
-\subsection{Bibliography}\label{bibliography}
+\section{Bibliography}\label{bibliography}
 
 \begin{enumerate}
 \tightlist
@@ -732,7 +732,7 @@ Next:
 \href{https://bartoszmilewski.com/2015/04/07/natural-transformations/}{Natural
 Transformations}.
 
-\subsection{Acknowledgments}\label{acknowledgments}
+\section{Acknowledgments}\label{acknowledgments}
 
 I'd like to thank Gershom Bazerman for checking my math and logic, and
 André van Meulebrouck, who has been volunteering his editing help
diff --git a/src/content/2.1/Declarative Programming.tex b/src/content/2.1/Declarative Programming.tex
index 29c72d8..a9e57ec 100644
--- a/src/content/2.1/Declarative Programming.tex	
+++ b/src/content/2.1/Declarative Programming.tex	
@@ -208,7 +208,7 @@ Next
 \href{https://bartoszmilewski.com/2015/04/15/limits-and-colimits/}{Limits
 and Colimits}.
 
-\subsection{Acknowledgments}\label{acknowledgments}
+\section{Acknowledgments}\label{acknowledgments}
 
 I'd like to thank Gershom Bazerman for checking my math and logic, and
 André van Meulebrouck, who has been volunteering his editing help.\\
diff --git a/src/content/2.2/Limits and Colimits.tex b/src/content/2.2/Limits and Colimits.tex
index 359640b..39bec8b 100644
--- a/src/content/2.2/Limits and Colimits.tex	
+++ b/src/content/2.2/Limits and Colimits.tex	
@@ -158,7 +158,7 @@ diagram is the product of two objects. The product (together with the
 two projections) contains the information about both objects. And being
 universal means that it has no extraneous junk.
 
-\subsection{Limit as a Natural
+\section{Limit as a Natural
 Isomorphism}\label{limit-as-a-natural-isomorphism}
 
 There is still something unsatisfying about this definition of a limit.
@@ -339,7 +339,7 @@ As a preview of coming attractions, let me mention that the set
 category; so our natural isomorphism relates two hom-sets, which points
 at an even more general relationship called an adjunction.
 
-\subsection{Examples of Limits}\label{examples-of-limits}
+\section{Examples of Limits}\label{examples-of-limits}
 
 We've seen that the categorical product is a limit of a diagram
 generated by a simple category we called \textbf{2}.
@@ -571,7 +571,7 @@ twice :: (t -> t) -> t -> t
 
 with \code{t} a free type variable.
 
-\subsection{Colimits}\label{colimits}
+\section{Colimits}\label{colimits}
 
 Just like all constructions in category theory, limits have their dual
 image in opposite categories. When you invert the direction of all
@@ -601,7 +601,7 @@ The dual of the pullback is called the \newterm{pushout}. It's based on a
 diagram called a span, generated by the category
 \code{1\textless{}-2-\textgreater{}3}.
 
-\subsection{Continuity}\label{continuity}
+\section{Continuity}\label{continuity}
 
 I said previously that functors come close to the idea of continuous
 mappings of categories, in the sense that they never break existing
@@ -680,7 +680,7 @@ calculus. In calculus limits and continuity are defined in terms of open
 neighborhoods. Open sets, which define topology, form a category (a
 poset).
 
-\subsection{Challenges}\label{challenges}
+\section{Challenges}\label{challenges}
 
 \begin{enumerate}
 \tightlist
@@ -707,7 +707,7 @@ poset).
 Next: \href{https://bartoszmilewski.com/2015/07/21/free-monoids/}{Free
 Monoids}.
 
-\subsection{Acknowledgments}\label{acknowledgments}
+\section{Acknowledgments}\label{acknowledgments}
 
 I'd like to thank Gershom Bazerman for checking my math and logic, and
 André van Meulebrouck, who has been volunteering his editing help.\\
diff --git a/src/content/2.3/Free Monoids.tex b/src/content/2.3/Free Monoids.tex
index 1621153..78ab5b8 100644
--- a/src/content/2.3/Free Monoids.tex	
+++ b/src/content/2.3/Free Monoids.tex	
@@ -67,7 +67,7 @@ identifications --- just enough to uphold the laws --- is called a free
 construction. What we have just done is to construct a \newterm{free
 monoid} from the set of generators \code{\{a,\ b\}}.
 
-\subsection{Free Monoid in Haskell}\label{free-monoid-in-haskell}
+\section{Free Monoid in Haskell}\label{free-monoid-in-haskell}
 
 A two-element set in Haskell is equivalent to the type \code{Bool},
 and the free monoid generated by this set is equivalent to the type
@@ -114,7 +114,7 @@ free monoid by identifying more than the minimum number of elements
 required by the laws? I'll show you that this follows directly from the
 universal construction.
 
-\subsection{Free Monoid Universal
+\section{Free Monoid Universal
 Construction}\label{free-monoid-universal-construction}
 
 If you recall our previous experiences with universal constructions, you
@@ -262,7 +262,7 @@ have been made.
 
 We'll come back to free monoids when we talk about adjunctions.
 
-\subsection{Challenges}\label{challenges}
+\section{Challenges}\label{challenges}
 
 \begin{enumerate}
 \item
@@ -297,7 +297,7 @@ Next:
 \href{https://bartoszmilewski.com/2015/07/29/representable-functors/}{Representable
 Functors}.
 
-\subsection{Acknowledgments}\label{acknowledgments}
+\section{Acknowledgments}\label{acknowledgments}
 
 I'd like to thank Gershom Bazerman for checking my math and logic, and
 André van Meulebrouck, who has been volunteering his editing help
diff --git a/src/content/2.4/Representable Functors.tex b/src/content/2.4/Representable Functors.tex
index 79611d5..fb66ca9 100644
--- a/src/content/2.4/Representable Functors.tex	
+++ b/src/content/2.4/Representable Functors.tex	
@@ -51,7 +51,7 @@ categories, but you can compare sets of apples against sets of oranges.
 Often transforming a categorical problem into a set-theoretical problem
 gives us the necessary insight or even lets us prove valuable theorems.
 
-\subsection{The Hom Functor}\label{the-hom-functor}
+\section{The Hom Functor}\label{the-hom-functor}
 
 Every category comes equipped with a canonical family of mappings to
 \textbf{Set}. Those mappings are in fact functors, so they preserve the
@@ -169,7 +169,7 @@ fact succintly as:
 C(-, =) :: Cop × C -> Set
 \end{verbatim}
 
-\subsection{Representable Functors}\label{representable-functors}
+\section{Representable Functors}\label{representable-functors}
 
 We've seen that, for every choice of an object \code{a} in \emph{C},
 we get a functor from \emph{C} to \textbf{Set}. This kind of
@@ -382,7 +382,7 @@ valuable in practice. So, surprisingly, even though it's not concerned
 with performance at all, category theory provides ample opportunities to
 explore alternative implementations that have practical value.
 
-\subsection{Challenges}\label{challenges}
+\section{Challenges}\label{challenges}
 
 \begin{enumerate}
 \item
@@ -409,7 +409,7 @@ Pair a = Pair a a
   \code{tabulate} and \code{index}.
 \end{enumerate}
 
-\subsection{Bibliography}\label{bibliography}
+\section{Bibliography}\label{bibliography}
 
 \begin{enumerate}
 \tightlist
@@ -423,7 +423,7 @@ Next:
 \href{https://bartoszmilewski.com/2015/09/01/the-yoneda-lemma/}{The
 Yoneda Lemma}.
 
-\subsection{Acknowledgments}\label{acknowledgments}
+\section{Acknowledgments}\label{acknowledgments}
 
 I'd like to thank Gershom Bazerman for checking my math and logic, and
 André van Meulebrouck, who has been volunteering his editing help
diff --git a/src/content/2.5/The Yoneda Lemma.tex b/src/content/2.5/The Yoneda Lemma.tex
index ab143d2..3f5784c 100644
--- a/src/content/2.5/The Yoneda Lemma.tex	
+++ b/src/content/2.5/The Yoneda Lemma.tex	
@@ -238,7 +238,7 @@ hom-functor through a lossy transformation. Such a transformation may
 not only lose information, but it may also cover only a small part of
 the image of the functor \code{F} in \textbf{Set}.
 
-\subsection{Yoneda in Haskell}\label{yoneda-in-haskell}
+\section{Yoneda in Haskell}\label{yoneda-in-haskell}
 
 We have already encountered the hom-functor in Haskell under the guise
 of the reader functor:
@@ -338,7 +338,7 @@ of spaghetti code from interacting stateful handlers. As we'll see
 later, judicious use of functors and monads can restore some
 compositional properties of CPS.
 
-\subsection{Co-Yoneda}\label{co-yoneda}
+\section{Co-Yoneda}\label{co-yoneda}
 
 As usual, we get a bonus construction by inverting the direction of
 arrows. The Yoneda lemma can be applied to the opposite category
@@ -366,7 +366,7 @@ forall x . (x -> a) -> F x ≅ F a
 Notice that in some literature it's the contravariant version that's
 called the Yoneda lemma.
 
-\subsection{Challenges}\label{challenges}
+\section{Challenges}\label{challenges}
 
 \begin{enumerate}
 \item
@@ -393,13 +393,13 @@ psi :: F a -> (forall x . (a -> x) -> F x) psi fa h = fmap h fa
   functor.
 \end{enumerate}
 
-\subsection{Bibliography}\label{bibliography}
+\section{Bibliography}\label{bibliography}
 
 Next:
 \href{https://bartoszmilewski.com/2015/10/28/yoneda-embedding/}{Yoneda
 Embedding}.
 
-\subsection{Acknowledgments}\label{acknowledgments}
+\section{Acknowledgments}\label{acknowledgments}
 
 I'd like to thank Gershom Bazerman for checking my math and logic, and
 André van Meulebrouck, who has been volunteering his editing help
diff --git a/src/content/2.6/Yoneda Embedding.tex b/src/content/2.6/Yoneda Embedding.tex
index ded162d..2eaa5cb 100644
--- a/src/content/2.6/Yoneda Embedding.tex	
+++ b/src/content/2.6/Yoneda Embedding.tex	
@@ -96,7 +96,7 @@ Notice that this doesn't mean that \code{F} is a bijection on
 image of \code{F}, and we can't say anything about hom-sets for those
 objects.
 
-\subsection{The Embedding}\label{the-embedding}
+\section{The Embedding}\label{the-embedding}
 
 The (contravariant) functor we have just described, the functor that
 maps objects in \emph{C} to functors in \code{{[}C,\ Set{]}}:
@@ -134,7 +134,7 @@ is given by:
 Again, mathematicians know a lot about the category of presheaves, so
 being able to embed an arbitrary category in it is a big win.
 
-\subsection{Application to Haskell}\label{application-to-haskell}
+\section{Application to Haskell}\label{application-to-haskell}
 
 In Haskell, the Yoneda embedding can be represented as the isomorphism
 between natural transformations amongst reader functors on the one hand,
@@ -186,7 +186,7 @@ provides a very useful
 \href{https://bartoszmilewski.com/2015/07/13/from-lenses-to-yoneda-embedding/}{representation
 of lenses} from the \code{Control.Lens} library.
 
-\subsection{Preorder Example}\label{preorder-example}
+\section{Preorder Example}\label{preorder-example}
 
 This example was suggested by Robert Harper. It's the application of the
 Yoneda embedding to a category defined by a preorder. A preorder is a
@@ -267,7 +267,7 @@ must also be below \code{b}. Conversely, when you substitute
 \code{a\ \textless{}=\ b}. But you must admit that arriving at this
 result through the Yoneda embedding is much more exciting.
 
-\subsection{Naturality}\label{naturality}
+\section{Naturality}\label{naturality}
 
 The Yoneda lemma establishes the isomorphism between the set of natural
 transformations and an object in \textbf{Set}. Natural transformations
@@ -325,7 +325,7 @@ mechanical. It follows from the fact that our isomorphism is built up
 from functors and natural transformations. There is simply no way for it
 to go wrong.
 
-\subsection{Challenges}\label{challenges}
+\section{Challenges}\label{challenges}
 
 \begin{enumerate}
 \tightlist
@@ -353,7 +353,7 @@ Next:
 \href{https://bartoszmilewski.com/2015/11/17/its-all-about-morphisms/}{It's
 All About Morphisms}.
 
-\subsection{Acknowledgments}\label{acknowledgments}
+\section{Acknowledgments}\label{acknowledgments}
 
 I'd like to thank Gershom Bazerman for checking my math and logic.\\
 \href{https://twitter.com/BartoszMilewski}{Follow @BartoszMilewski}
diff --git a/src/content/3.1/It’s All About Morphisms.tex b/src/content/3.1/It’s All About Morphisms.tex
index f8ceac4..0a53ab7 100644
--- a/src/content/3.1/It’s All About Morphisms.tex	
+++ b/src/content/3.1/It’s All About Morphisms.tex	
@@ -14,7 +14,7 @@ hom-sets. Also, you'll see that adjunctions provide a more general
 language to describe a lot of constructions we've studied before, so it
 might help to review them too.
 
-\subsection{Functors}\label{functors}
+\section{Functors}\label{functors}
 
 To begin with, you should really think of functors as mappings of
 morphisms --- the view that's emphasized in the Haskell definition of
@@ -27,7 +27,7 @@ be composed. So if we want the composition of morphisms to be mapped to
 the composition of \newterm{lifted} morphisms, the mapping of their
 endpoints is pretty much determined.
 
-\subsection{Commuting Diagrams}\label{commuting-diagrams}
+\section{Commuting Diagrams}\label{commuting-diagrams}
 
 A lot of properties of morphisms are expressed in terms of commuting
 diagrams. If a particular morphism can be described as a composition of
@@ -52,7 +52,7 @@ the mapping of functors. This way commutativity is reduced to the role
 of the assembly language for the higher level language of natural
 transformations.
 
-\subsection{Natural Transformations}\label{natural-transformations}
+\section{Natural Transformations}\label{natural-transformations}
 
 In general, natural transformations are very convenient whenever we need
 a mapping from morphisms to commuting squares. Two opposing sides of a
@@ -109,7 +109,7 @@ that defines the diagram in \emph{C}. Both functors \code{F} and
 happens that this particular natural transformation between \code{F}
 and \code{G} is an \newterm{isomorphism}.
 
-\subsection{Natural Isomorphisms}\label{natural-isomorphisms}
+\section{Natural Isomorphisms}\label{natural-isomorphisms}
 
 A natural isomorphism --- which is a natural transformation whose every
 component is reversible --- is category theory's way of saying that
@@ -118,7 +118,7 @@ be an isomorphism between objects --- a morphism that has the inverse.
 If you visualize functor images as sheets, a natural isomorphism is a
 one-to-one invertible mapping between those sheets.
 
-\subsection{Hom-Sets}\label{hom-sets}
+\section{Hom-Sets}\label{hom-sets}
 
 But what are morphisms? They do have more structure than objects: unlike
 objects, morphisms have two ends. But if you fix the source and the
@@ -154,7 +154,7 @@ h&apos; ∘ F f ≠ h&apos; ∘ F g
 
 where \code{h\&apos;} is not in the image of \code{F}.
 
-\subsection{Hom-Set Isomorphisms}\label{hom-set-isomorphisms}
+\section{Hom-Set Isomorphisms}\label{hom-set-isomorphisms}
 
 A lot of categorical constructions rely on isomorphisms between
 hom-sets. But since hom-sets are just sets, a plain isomorphism between
@@ -196,7 +196,7 @@ This is no coincidence --- we'll see next that these are just different
 examples of adjunctions, which are defined as natural isomorphisms of
 hom-sets.
 
-\subsection{Asymmetry of Hom-Sets}\label{asymmetry-of-hom-sets}
+\section{Asymmetry of Hom-Sets}\label{asymmetry-of-hom-sets}
 
 There is one more observation that will help us understand adjunctions.
 Hom-sets are, in general, not symmetric. A hom-set \code{C(a,\ b)} is
@@ -219,7 +219,7 @@ generalization of a preoder.
 A preorder is a thin category --- all hom-sets are either singletons or
 empty. We can visualize a general category as a ``thick'' preorder.
 
-\subsection{Challenges}\label{challenges}
+\section{Challenges}\label{challenges}
 
 \begin{enumerate}
 \tightlist
@@ -238,7 +238,7 @@ empty. We can visualize a general category as a ``thick'' preorder.
 Next:
 \href{https://bartoszmilewski.com/2016/04/18/adjunctions/}{Adjunctions}.
 
-\subsection{Acknowledgments}\label{acknowledgments}
+\section{Acknowledgments}\label{acknowledgments}
 
 I'd like to thank Gershom Bazerman for checking my math and logic, and
 André van Meulebrouck, who has been volunteering his editing help
diff --git a/src/content/3.10/Ends and Coends.tex b/src/content/3.10/Ends and Coends.tex
index 4148b7c..0487671 100644
--- a/src/content/3.10/Ends and Coends.tex	
+++ b/src/content/3.10/Ends and Coends.tex	
@@ -88,7 +88,7 @@ from \code{p\ a\ a} to \code{p\ a\ b}:
 dimap id f paa :: p a b
 \end{verbatim}
 
-\subsection{Dinatural Transformations}\label{dinatural-transformations}
+\section{Dinatural Transformations}\label{dinatural-transformations}
 
 Since profunctors are functors, we can define natural transformations
 between them in the standard way. In many cases, though, it's enough to
@@ -123,7 +123,7 @@ Notice that a component of a natural transformation \code{α} in
 indexed by one object, since it only maps diagonal elements of the
 respective profunctors.
 
-\subsection{Ends}\label{ends}
+\section{Ends}\label{ends}
 
 We are now ready to advance from ``algebra'' to what could be considered
 the ``calculus'' of category theory. The calculus of ends (and coends)
@@ -251,7 +251,7 @@ Ends can also be defined for target categories other than \textbf{Set},
 but here we'll only consider \textbf{Set}-valued profunctors and their
 ends.
 
-\subsection{Ends as Equalizers}\label{ends-as-equalizers}
+\section{Ends as Equalizers}\label{ends-as-equalizers}
 
 The commutation condition in the definition of the end can be written
 using an equalizer. First, let's define two functions (I'm using Haskell
@@ -290,7 +290,7 @@ that the equalizer picks the largest subset on which two functions are
 equal. In this case it picks the subset of the product of all diagonal
 elements for which the wedge diagrams commute.
 
-\subsection{Natural Transformations as
+\section{Natural Transformations as
 Ends}\label{natural-transformations-as-ends}
 
 The most important example of an end is the set of natural
@@ -344,7 +344,7 @@ idb ∘ τb ∘ F f
 Their equality, demanded by the wedge condition, is nothing but the
 naturality condition for \code{τ}.
 
-\subsection{Coends}\label{coends}
+\section{Coends}\label{coends}
 
 As expected, the dual to an end is called a coend. It is constructed
 from a dual to a wedge called a cowedge (pronounced co-wedge, not
@@ -474,7 +474,7 @@ statement, with a tuple of handlers, one for every type present in the
 sum. Here, the sum type is replaced by a coend, and a family of handlers
 becomes an end, or a polymorphic function.
 
-\subsection{Ninja Yoneda Lemma}\label{ninja-yoneda-lemma}
+\section{Ninja Yoneda Lemma}\label{ninja-yoneda-lemma}
 
 The set of natural transformations that appears in the Yoneda lemma may
 be encoded using an end, resulting in the following formulation:
@@ -548,7 +548,7 @@ isomorphism:
 ∫ z C(a, z) × F z ≅ F a
 \end{verbatim}
 
-\subsection{Profunctor Composition}\label{profunctor-composition}
+\section{Profunctor Composition}\label{profunctor-composition}
 
 Let's explore further the idea that a profunctor describes a relation
 --- more precisely, a proof-relevant relation, meaning that the set
diff --git a/src/content/3.11/Kan Extensions.tex b/src/content/3.11/Kan Extensions.tex
index d2e68f6..d6e9dce 100644
--- a/src/content/3.11/Kan Extensions.tex	
+++ b/src/content/3.11/Kan Extensions.tex	
@@ -84,7 +84,7 @@ But, importantly, we are free to replace the trivial category \textbf{1}
 with an arbitrary category \emph{A}, and the definition of the right Kan
 extension remains valid.
 
-\subsection{Right Kan Extension}\label{right-kan-extension}
+\section{Right Kan Extension}\label{right-kan-extension}
 
 The right Kan extension of the functor \code{D::I-\textgreater{}C}
 along the functor \code{K::I-\textgreater{}A} is a functor
@@ -148,7 +148,7 @@ is not injective on objects or not faithful on hom-sets, as in the
 example of the limit. In that case, the Kan extension tries its best to
 extrapolate the lost information.
 
-\subsection{Kan Extension as
+\section{Kan Extension as
 Adjunction}\label{kan-extension-as-adjunction}
 
 Now suppose that the right Kan extension exists for any \code{D} (and
@@ -226,7 +226,7 @@ The adjunction formula is an important result because, as we'll see
 soon, we can calculate Kan extensions using ends (coends), thus giving
 us practical means of finding right (and left) adjoints.
 
-\subsection{Left Kan Extension}\label{left-kan-extension}
+\section{Left Kan Extension}\label{left-kan-extension}
 
 There is a dual construction that gives us the left Kan extension. To
 build some intuition, we'll can start with the definition of a colimit
@@ -308,7 +308,7 @@ Combining the two results, we get:
 RanKIC ⊣ K ⊣ LanKIC
 \end{verbatim}
 
-\subsection{Kan Extensions as Ends}\label{kan-extensions-as-ends}
+\section{Kan Extensions as Ends}\label{kan-extensions-as-ends}
 
 The real power of Kan extensions comes from the fact that they can be
 calculated using ends (and coends). For simplicity, we'll restrict our
@@ -441,7 +441,7 @@ hand side of the adjunction we set out to prove:
 These kinds of calculations using ends, coends, and the Yoneda lemma are
 pretty typical for the ``calculus'' of ends.
 
-\subsection{Kan Extensions in Haskell}\label{kan-extensions-in-haskell}
+\section{Kan Extensions in Haskell}\label{kan-extensions-in-haskell}
 
 The end/coend formulas for Kan extensions can be easily translated to
 Haskell. Let's start with the right extension:
@@ -551,7 +551,7 @@ repackaged the container using the natural transformation between the
 identity functor and the pair functor, and (3) called the function
 \code{f}.
 
-\subsection{Free Functor}\label{free-functor}
+\section{Free Functor}\label{free-functor}
 
 An interesting application of Kan extensions is the construction of a
 free functor. It's the solution to the following practical problem:
diff --git a/src/content/3.12/Enriched Categories.tex b/src/content/3.12/Enriched Categories.tex
index 7c70350..f597fd8 100644
--- a/src/content/3.12/Enriched Categories.tex	
+++ b/src/content/3.12/Enriched Categories.tex	
@@ -42,7 +42,7 @@ enriched categories, and that's because a very useful online source of
 categorical knowledge, the \href{https://ncatlab.org/}{nLab}, is written
 mostly in terms of enriched categories.
 
-\subsection{Why Monoidal Category?}\label{why-monoidal-category}
+\section{Why Monoidal Category?}\label{why-monoidal-category}
 
 When constructing an enriched category we have to keep in mind that we
 should be able to recover the usual definitions when we replace the
@@ -81,7 +81,7 @@ tensor product.
 As you can see, objects taken from some monoidal category \emph{V} are
 good candidates for hom-set replacement.
 
-\subsection{Monoidal Category}\label{monoidal-category}
+\section{Monoidal Category}\label{monoidal-category}
 
 We've talked about monoidal categories before, but it's worth restating
 the definition. A monoidal category defines a tensor product that is a
@@ -166,7 +166,7 @@ example of a category that is not biclosed is the category of
 endofunctors in \textbf{Set}, with functor composition serving as tensor
 product. That's the category we used to define monads.
 
-\subsection{Enriched Category}\label{enriched-category}
+\section{Enriched Category}\label{enriched-category}
 
 A category \emph{C} enriched over a monoidal category \emph{V} replaces
 hom-sets with hom-objects. To every pair of objects \code{a} and
@@ -207,7 +207,7 @@ Unit laws are likewise expressed in terms of unitors:
 
 \includegraphics[width=4.65625in]{images/leftid.jpg}
 
-\subsection{Preorders}\label{preorders}
+\section{Preorders}\label{preorders}
 
 A preorder is defined as a thin category, one in which every hom-set is
 either empty or a singleton. We interpret a non-empty set
@@ -245,7 +245,7 @@ There is only one morphism going from 1, and that's the identity
 preorder. So both transitivity and reflexivity are automatically
 enforced, if we implement a preorder as an enriched category.
 
-\subsection{Metric Spaces}\label{metric-spaces}
+\section{Metric Spaces}\label{metric-spaces}
 
 An interesting example is due to
 \href{http://www.tac.mta.ca/tac/reprints/articles/1/tr1.pdf}{William
@@ -306,7 +306,7 @@ to \code{c}. But that's just the standard triangle inequality. Check!
 By re-casting the metric space in terms of an enriched category, we get
 the triangle inequality and the zero self-distance ``for free.''
 
-\subsection{Enriched Functors}\label{enriched-functors}
+\section{Enriched Functors}\label{enriched-functors}
 
 The definition of a functor involves the mapping of morphisms. In the
 enriched setting, we don't have the notion of individual morphisms, so
@@ -336,7 +336,7 @@ morphisms in \emph{V} that ``select'' the identity:
 
 \includegraphics[width=4.04167in]{images/functorid.jpg}
 
-\subsection{Self Enrichment}\label{self-enrichment}
+\section{Self Enrichment}\label{self-enrichment}
 
 A closed symmetric monoidal category may be self-enriched by replacing
 hom-sets with internal homs (see the definition above). To make this
@@ -426,7 +426,7 @@ equivalent. Now we also know that, through self-enrichment, we can use
 the exponential set as the hom-object and express composition in terms
 of cartesian products of exponential objects.
 
-\subsection{Relation to 2-Categories}\label{relation-to-2-categories}
+\section{Relation to 2-Categories}\label{relation-to-2-categories}
 
 I talked about 2-categories in the context of \textbf{Cat}, the category
 of (small) categories. The morphisms between categories are functors,
diff --git a/src/content/3.13/Topoi.tex b/src/content/3.13/Topoi.tex
index d4295e1..702517b 100644
--- a/src/content/3.13/Topoi.tex
+++ b/src/content/3.13/Topoi.tex
@@ -37,7 +37,7 @@ category that has just the right properties to serve as a replacement
 for set theory is called a \newterm{topos} (plural: topoi), and it
 provides, among other things, a generalized notion of a subset.
 
-\subsection{Subobject Classifier}\label{subobject-classifier}
+\section{Subobject Classifier}\label{subobject-classifier}
 
 Let's start by trying to express the idea of a subset using functions
 rather than elements. Any function \code{f} from some set \code{a}
@@ -202,7 +202,7 @@ This happens to be a natural isomorphism of two functors. In other
 words, \code{Sub(-)} is a representable (contravariant) functor whose
 representation is the object Ω.
 
-\subsection{Topos}\label{topos}
+\section{Topos}\label{topos}
 
 A topos is a category that:
 
@@ -227,7 +227,7 @@ It would be tempting to define the subobject classifier as a coproduct
 \textbf{Set}--- but we want to be more general than that. Topoi in which
 this is true are called Boolean.
 
-\subsection{Topoi and Logic}\label{topoi-and-logic}
+\section{Topoi and Logic}\label{topoi-and-logic}
 
 In set theory, a characteristic function may be interpreted as defining
 a property of the elements of a set --- a \newterm{predicate} that is true
@@ -262,7 +262,7 @@ Next:
 \href{https://bartoszmilewski.com/2017/08/26/lawvere-theories/}{Lawvere
 Theories}.
 
-\subsection{Challenges}\label{challenges}
+\section{Challenges}\label{challenges}
 
 \begin{enumerate}
 \tightlist
diff --git a/src/content/3.14/Lawvere Theories.tex b/src/content/3.14/Lawvere Theories.tex
index c8e0bee..7674f93 100644
--- a/src/content/3.14/Lawvere Theories.tex	
+++ b/src/content/3.14/Lawvere Theories.tex	
@@ -10,7 +10,7 @@ monads. But there is an alternative universe in which, by chance,
 Eugenio Moggi turned his attention to Lawvere theories rather than
 monads. Let's explore that universe.
 
-\subsection{Universal Algebra}\label{universal-algebra}
+\section{Universal Algebra}\label{universal-algebra}
 
 There are many ways of describing algebras at various levels of
 abstraction. We try to find a general language to describe things like
@@ -77,7 +77,7 @@ the roadmap:
 
 \includegraphics[width=5.31250in]{images/lawvere1.png}
 
-\subsection{Lavwere Theories}\label{lavwere-theories}
+\section{Lavwere Theories}\label{lavwere-theories}
 
 All Lawvere theories share a common backbone. All objects in a Lawvere
 theory are generated from just one object using products (really, just
@@ -214,7 +214,7 @@ At this point it would be very helpful to present a non-trivial example
 of a Lawvere theory, but it would be hard to explain it without first
 understanding what models are.
 
-\subsection{Models of Lawvere
+\section{Models of Lawvere
 Theories}\label{models-of-lawvere-theories}
 
 The key to understand Lawvere theories is to realize that one such
@@ -305,7 +305,7 @@ function \code{M\ 1\ -\textgreater{}\ N\ 1} induces a natural
 transformation between the two models \code{M} and \code{N}.
 Therefore \code{Mod(Fop,\ Set)} is equivalent to \textbf{Set}.
 
-\subsection{The Theory of Monoids}\label{the-theory-of-monoids}
+\section{The Theory of Monoids}\label{the-theory-of-monoids}
 
 The simplest nontrivial example of a Lawvere theory describes the
 structure of monoids. It is a single theory that distills the structure
@@ -358,7 +358,7 @@ The category of \newterm{models} of the Lawvere theory for monoids,
 \code{Mod(LMon,\ Set)}, is equivalent to the category of all monoids,
 \textbf{Mon}.
 
-\subsection{Lawvere Theories and
+\section{Lawvere Theories and
 Monads}\label{lawvere-theories-and-monads}
 
 As you may remember, algebraic theories can be described using monads
@@ -494,7 +494,7 @@ finitary, with the notable exception of the continuation monad. It is
 possible to to extend the notion of Lawvere theory beyond finitary
 operations.
 
-\subsection{Monads as Coends}\label{monads-as-coends}
+\section{Monads as Coends}\label{monads-as-coends}
 
 Let's explore the coend formula in more detail.
 
@@ -635,7 +635,7 @@ T a = a × L(1, 1) = a
 
 which is the identity monad.
 
-\subsection{Lawvere Theory of Side
+\section{Lawvere Theory of Side
 Effects}\label{lawvere-theory-of-side-effects}
 
 Since there is such a strong connection between monads and Lawvere
@@ -703,7 +703,7 @@ Next:
 \href{https://bartoszmilewski.com/2017/09/06/monads-monoids-and-categories/}{Monads,
 Monoids, and Categories}.
 
-\subsection{Challenges}\label{challenges}
+\section{Challenges}\label{challenges}
 
 \begin{enumerate}
 \tightlist
@@ -724,8 +724,8 @@ Monoids, and Categories}.
   the left Kan extension of its own restriction.
 \end{enumerate}
 
-\subsection{Acknowledgments}\label{acknowledgments}
+\section{Acknowledgments}\label{acknowledgments}
 
 I'm grateful to Gershom Bazerman for many useful comments.
 
-\subsection{Further Reading}\label{further-reading}
+\section{Further Reading}\label{further-reading}
diff --git a/src/content/3.15/Monads, Monoids, and Categories.tex b/src/content/3.15/Monads, Monoids, and Categories.tex
index f3ff771..1fd50ba 100644
--- a/src/content/3.15/Monads, Monoids, and Categories.tex	
+++ b/src/content/3.15/Monads, Monoids, and Categories.tex	
@@ -18,7 +18,7 @@ As it turns out they are all interrelated, one leading to another in a
 never-ending cycle of abstractions. I decided that showing these
 interconnections might be a good way to end this book.
 
-\subsection{Bicategories}\label{bicategories}
+\section{Bicategories}\label{bicategories}
 
 One of the most difficult aspects of category theory is the constant
 switching of perspectives. Take the category of sets, for instance. We
@@ -185,7 +185,7 @@ where 0-cells are categories, 1-cells are profunctors, and 2-cells are
 natural transformations. The composition of profunctors was given by a
 coend.
 
-\subsection{Monads}\label{monads}
+\section{Monads}\label{monads}
 
 By now you should be pretty familiar with the definition of a monad as a
 monoid in the category of endofunctors. Let's revisit this definition
@@ -305,7 +305,7 @@ one-to-one correspondence). So it's really just a set and a few
 functions. Considering the pivotal role that category theory plays in
 all of mathematics, this is a very humbling realization.
 
-\subsection{Challenges}\label{challenges}
+\section{Challenges}\label{challenges}
 
 \begin{enumerate}
 \tightlist
@@ -321,4 +321,4 @@ all of mathematics, this is a very humbling realization.
   What's a monad algebra for a monad in \textbf{Span}?
 \end{enumerate}
 
-\subsection{Bibliography}\label{bibliography}
+\section{Bibliography}\label{bibliography}
diff --git a/src/content/3.2/Adjunctions.tex b/src/content/3.2/Adjunctions.tex
index e6e1b74..55dde8c 100644
--- a/src/content/3.2/Adjunctions.tex
+++ b/src/content/3.2/Adjunctions.tex
@@ -31,7 +31,7 @@ swap :: (a,b) -> (b,a) swap (a,b) = (b,a)
 
 \code{swap} happens to be its own inverse.
 
-\subsection{Adjunction and Unit/Counit
+\section{Adjunction and Unit/Counit
 Pair}\label{adjunction-and-unitcounit-pair}
 
 When we talk about categories being isomorphic, we express this in terms
@@ -241,7 +241,7 @@ and \code{u} is a function, here on type constructors). Conversely,
 I'll explain in a moment why, in Haskell, we can impose the condition
 that the right adjoint \code{u} be a \newterm{representable} functor.
 
-\subsection{Adjunctions and Hom-Sets}\label{adjunctions-and-hom-sets}
+\section{Adjunctions and Hom-Sets}\label{adjunctions-and-hom-sets}
 
 There is an equivalent definition of the adjunction in terms of natural
 isomorphisms of hom-sets. This definition ties nicely with universal
@@ -429,7 +429,7 @@ C(L (), -) ≅ R
 
 which shows that \code{R} is indeed representable.
 
-\subsection{Product from Adjunction}\label{product-from-adjunction}
+\section{Product from Adjunction}\label{product-from-adjunction}
 
 We have previously introduced several concepts using universal
 constructions. Many of those concepts, when defined globally, are easier
@@ -607,7 +607,7 @@ for instance:
 (,) Int Bool ~ (Int, Bool)
 \end{verbatim}
 
-\subsection{Exponential from
+\section{Exponential from
 Adjunction}\label{exponential-from-adjunction}
 
 The exponential \code{ba}, or the function object \code{a⇒b}, can be
@@ -670,7 +670,7 @@ unique object, up to isomorphism. That's why we have ``the'' product and
 ``the'' exponential. This property translates to adjunctions as well: if
 a functor has an adjoint, this adjoint is unique up to isomorphism.
 
-\subsection{Challenges}\label{challenges}
+\section{Challenges}\label{challenges}
 
 \begin{enumerate}
 \item
@@ -700,7 +700,7 @@ Next:
 \href{https://bartoszmilewski.com/2016/06/15/freeforgetful-adjunctions/}{Free/Forgetful
 Adjunctions}.
 
-\subsection{Acknowledgments}\label{acknowledgments}
+\section{Acknowledgments}\label{acknowledgments}
 
 I'd like to thank Edward Kmett and Gershom Bazerman for checking my math
 and logic, and André van Meulebrouck, who has been volunteering his
diff --git "a/src/content/3.3/Free\\Forgetful Adjunctions.tex" "b/src/content/3.3/Free\\Forgetful Adjunctions.tex"
index 3f854be..023075c 100644
--- "a/src/content/3.3/Free\\Forgetful Adjunctions.tex"	
+++ "b/src/content/3.3/Free\\Forgetful Adjunctions.tex"	
@@ -134,7 +134,7 @@ For simplicity I used the type \code{Int} rather than
 \code{replicate} creates a list of length \code{n} pre-filled with a
 given value --- here, the unit.
 
-\subsection{Some Intuitions}\label{some-intuitions}
+\section{Some Intuitions}\label{some-intuitions}
 
 What follows are some hand-waving arguments. Those kind of arguments are
 far from rigorous, but they help in forming intuitions.
@@ -238,7 +238,7 @@ instance, done in implementing matrix calculus, where eager evaluation
 would lead to lots of allocations of temporary arrays to store
 intermediate results.
 
-\subsection{Challenges}\label{challenges}
+\section{Challenges}\label{challenges}
 
 \begin{enumerate}
 \tightlist
@@ -253,7 +253,7 @@ Next:
 \href{https://bartoszmilewski.com/2016/11/21/monads-programmers-definition/}{Monads:
 Programmer's Definition}.
 
-\subsection{Acknowledgments}\label{acknowledgments}
+\section{Acknowledgments}\label{acknowledgments}
 
 I'd like to thank Gershom Bazerman for checking my math and logic, and
 André van Meulebrouck, who has been volunteering his editing help
diff --git a/src/content/3.4/Monads - Programmer’s Definition.tex b/src/content/3.4/Monads - Programmer’s Definition.tex
index c1bf130..fcae1ed 100644
--- a/src/content/3.4/Monads - Programmer’s Definition.tex	
+++ b/src/content/3.4/Monads - Programmer’s Definition.tex	
@@ -82,7 +82,7 @@ called the \code{do} notation for monadic composition. We'll see its
 use later. But first, let me explain why we need monadic composition in
 the first place.
 
-\subsection{The Kleisli Category}\label{the-kleisli-category}
+\section{The Kleisli Category}\label{the-kleisli-category}
 
 We have previously arrived at the
 \href{https://bartoszmilewski.com/2014/12/23/kleisli-categories/}{writer
@@ -180,7 +180,7 @@ tell :: w -> Writer w () tell s = Writer ((), s)
 
 We'll use it later as a building block for other monadic functions.
 
-\subsection{Fish Anatomy}\label{fish-anatomy}
+\section{Fish Anatomy}\label{fish-anatomy}
 
 When implementing the fish operator for different monads you quickly
 realize that a lot of code is repeated and can be easily factored out.
@@ -265,7 +265,7 @@ For completeness, here's \code{join} for the \code{Writer} monad:
 join :: Monoid w => Writer w (Writer w a) -> Writer w a join (Writer ((Writer (a, w&apos;)), w)) = Writer (a, w `mappend` w&apos;)
 \end{verbatim}
 
-\subsection{\texorpdfstring{The \code{do}
+\section{\texorpdfstring{The \code{do}
 Notation}{The do Notation}}\label{the-do-notation}
 
 One way of writing code using monads is to work with Kleisli arrows ---
diff --git a/src/content/3.5/Monads and Effects.tex b/src/content/3.5/Monads and Effects.tex
index a233cc7..186aebd 100644
--- a/src/content/3.5/Monads and Effects.tex	
+++ b/src/content/3.5/Monads and Effects.tex	
@@ -15,7 +15,7 @@ problem that would otherwise be solved using impure functions (e.g., by
 accessing and modifying some global state) was solved with pure
 functions.
 
-\subsection{The Problem}\label{the-problem}
+\section{The Problem}\label{the-problem}
 
 Here is a short list of similar problems, copied from
 \href{https://core.ac.uk/download/pdf/21173011.pdf}{Eugenio Moggi's
@@ -67,7 +67,7 @@ The next section is heavy on Haskell examples. Feel free to skim or even
 skip it if you're eager to get back to category theory or if you're
 already familiar with Haskell's implementation of monads.
 
-\subsection{The Solution}\label{the-solution}
+\section{The Solution}\label{the-solution}
 
 First, let's analyze the way we used the \code{Writer} monad. We
 started with a pure function that performed a certain task --- given
@@ -596,7 +596,7 @@ the action that prints ``World!'' receives, as input, the Universe in
 which ``Hello '' is already on the screen. It outputs a new Universe,
 with ``Hello World!'' on the screen.
 
-\subsection{Conclusion}\label{conclusion}
+\section{Conclusion}\label{conclusion}
 
 Of course I have just scratched the surface of monadic programming.
 Monads not only accomplish, with pure functions, what normally is done
diff --git a/src/content/3.6/Monads Categorically.tex b/src/content/3.6/Monads Categorically.tex
index 6df9bdd..9050126 100644
--- a/src/content/3.6/Monads Categorically.tex	
+++ b/src/content/3.6/Monads Categorically.tex	
@@ -196,7 +196,7 @@ multiplication μ, unit η, associativity, and unit laws. But our
 definition of a monoid is too narrow to describe a monad as a monoid. So
 let's generalize the notion of a monoid.
 
-\subsection{Monoidal Categories}\label{monoidal-categories}
+\section{Monoidal Categories}\label{monoidal-categories}
 
 Let's go back to the conventional definition of a monoid. It's a set
 with a binary operation and a special element called unit. In Haskell,
@@ -405,7 +405,7 @@ we'll see shortly, for the composition of endofunctors (and also for
 some more esoteric products like Day convolution). Monoidal categories
 will play an essential role in the formulation of enriched categories.
 
-\subsection{Monoid in a Monoidal
+\section{Monoid in a Monoidal
 Category}\label{monoid-in-a-monoidal-category}
 
 We are now ready to define a monoid in a more general setting of a
@@ -437,7 +437,7 @@ because we need to lift pairs of morphisms to form products such as
 straightforward generalization of our previous results for categorical
 products.
 
-\subsection{Monads as Monoids}\label{monads-as-monoids}
+\section{Monads as Monoids}\label{monads-as-monoids}
 
 Monoidal structures pop up in unexpected places. One such place is the
 functor category. If you squint a little, you might be able to see
@@ -504,7 +504,7 @@ All told, monad is just a monoid in the category of endofunctors.
 You might have seen it emblazoned on some t-shirts at functional
 programming conferences.
 
-\subsection{Monads from Adjunctions}\label{monads-from-adjunctions}
+\section{Monads from Adjunctions}\label{monads-from-adjunctions}
 
 An
 \href{https://bartoszmilewski.com/2016/04/18/adjunctions/}{adjunction},
diff --git a/src/content/3.7/Comonads.tex b/src/content/3.7/Comonads.tex
index 128b088..e17448f 100644
--- a/src/content/3.7/Comonads.tex
+++ b/src/content/3.7/Comonads.tex
@@ -50,7 +50,7 @@ In practice, we use slightly different primitives, as we'll see shortly.
 
 The question is, what's the use for comonads in programming?
 
-\subsection{Programming with Comonads}\label{programming-with-comonads}
+\section{Programming with Comonads}\label{programming-with-comonads}
 
 Let's compare the monad with the comonad. A monad provides a way of
 putting a value in a container using \code{return}. It doesn't give
@@ -70,7 +70,7 @@ result --- it embellishes it with context --- a co-Kleisli arrow takes a
 value together with a whole context and produces a result. It's an
 embodiment of \newterm{contextual computation}.
 
-\subsection{The Product Comonad}\label{the-product-comonad}
+\section{The Product Comonad}\label{the-product-comonad}
 
 Remember the reader monad? We introduced it to tackle the problem of
 implementing computations that need access to some read-only environment
@@ -123,7 +123,7 @@ later.
 It's easy to generalize the \code{Product} comonad to arbitrary
 product types including tuples and records.
 
-\subsection{Dissecting the
+\section{Dissecting the
 Composition}\label{dissecting-the-composition}
 
 Continuing the process of dualization, we could go ahead and dualize
@@ -214,7 +214,7 @@ new state of the current cell. To do that, it would look at its context
 \code{duplicate} to produce all possible foci and then we apply
 \code{f} to each of them.
 
-\subsection{The Stream Comonad}\label{the-stream-comonad}
+\section{The Stream Comonad}\label{the-stream-comonad}
 
 This process of shifting the focus from one element of the container to
 another is best illustrated with the example of an infinite stream. Such
@@ -298,7 +298,7 @@ The result is the stream of running averages.
 A stream is an example of a unidirectional, one-dimensional comonad. It
 can be easily made bidirectional or extended to two or more dimensions.
 
-\subsection{Comonad Categorically}\label{comonad-categorically}
+\section{Comonad Categorically}\label{comonad-categorically}
 
 Defining a comonad in category theory is a straightforward exercise in
 duality. As with the monad, we start with an endofunctor \code{T}. The
@@ -405,7 +405,7 @@ of endofunctors,
 
 The comonad is a comonoid in the category of endofunctors.
 
-\subsection{The Store Comonad}\label{the-store-comonad}
+\section{The Store Comonad}\label{the-store-comonad}
 
 Another important example of a comonad is the dual of the state monad.
 It's called the costate comonad or, alternatively, the store comonad.
@@ -533,7 +533,7 @@ returning the modified version of \code{a}. Similarly, \code{get}
 could be implemented to read the value of the \code{s} field from
 \code{a}. We'll explore these ideas more in the next section.
 
-\subsection{Challenges}\label{challenges}
+\section{Challenges}\label{challenges}
 
 \begin{enumerate}
 \tightlist
@@ -542,7 +542,7 @@ could be implemented to read the value of the \code{s} field from
   Hint: What type do you pick for \code{s}?
 \end{enumerate}
 
-\subsection{Acknowledgments}\label{acknowledgments}
+\section{Acknowledgments}\label{acknowledgments}
 
 I'm grateful to Edward Kmett for reading the draft of this post and
 pointing out flaws in my reasoning.
diff --git a/src/content/3.8/F-Algebras.tex b/src/content/3.8/F-Algebras.tex
index ffc1af1..e4cb610 100644
--- a/src/content/3.8/F-Algebras.tex
+++ b/src/content/3.8/F-Algebras.tex
@@ -154,7 +154,7 @@ can be evaluated using the evaluator of the algebra. So far we've only
 seen very simple expressions. We are often interested in more elaborate
 expressions that can be defined using recursion.
 
-\subsection{Recursion}\label{recursion}
+\section{Recursion}\label{recursion}
 
 One way to generate arbitrary expression trees is to replace the
 variable \code{a} inside the functor definition with recursion. For
@@ -254,7 +254,7 @@ unFix :: Fix f -> f (Fix f) unFix (Fix x) = x
 The two functions are the inverse of each other. We'll use these
 functions later.
 
-\subsection{Category of F-Algebras}\label{category-of-f-algebras}
+\section{Category of F-Algebras}\label{category-of-f-algebras}
 
 Here's the oldest trick in the book: Whenever you come up with a way of
 constructing some new objects, see if they form a category. Not
@@ -388,7 +388,7 @@ data Nat = Zero | Succ Nat
 A natural number is either zero or a successor of another number. This
 is known as the Peano representation for natural numbers.
 
-\subsection{Catamorphisms}\label{catamorphisms}
+\section{Catamorphisms}\label{catamorphisms}
 
 Let's rewrite the initiality condition using Haskell notation. We call
 the initial algebra \code{Fix\ f}. Its evaluator is the contructor
@@ -459,7 +459,7 @@ In general, an algebra for \code{NatF} defines a recurrence relation:
 the value of the current element in terms of the previous element. A
 catamorphism then evaluates the n-th element of that sequence.
 
-\subsection{Folds}\label{folds}
+\section{Folds}\label{folds}
 
 A list of \code{e} is the initial algebra of the following functor:
 
@@ -517,7 +517,7 @@ sum = foldr (\e s -> e + s) 0.0
 As you can see, \code{foldr} is just a convenient specialization of a
 catamorphism to lists.
 
-\subsection{Coalgebras}\label{coalgebras}
+\section{Coalgebras}\label{coalgebras}
 
 As usual, we have a dual construction of an F-coagebra, where the
 direction of the morphism is reversed:
@@ -655,7 +655,7 @@ We've seen before that \code{Store\ s} is also a comonad. It turns out
 that a well-behaved lens corresponds to a coalgebra that is compatible
 with the comonad structure. We'll talk about this in the next section.
 
-\subsection{Challenges}\label{challenges}
+\section{Challenges}\label{challenges}
 
 \begin{enumerate}
 \tightlist
diff --git a/src/content/3.9/Algebras for Monads.tex b/src/content/3.9/Algebras for Monads.tex
index 58d2af2..8cce94f 100644
--- a/src/content/3.9/Algebras for Monads.tex	
+++ b/src/content/3.9/Algebras for Monads.tex	
@@ -109,7 +109,7 @@ lists, and then fold the resulting list. Again, if we interpret
 binary operation is associative. These conditions are certainly
 fulfilled when \code{(a,\ f,\ z)} is a monoid.
 
-\subsection{T-algebras}\label{t-algebras}
+\section{T-algebras}\label{t-algebras}
 
 Since mathematicians prefer to call their monads \code{T}, they call
 algebras compatible with them T-algebras. T-algebras for a given monad T
@@ -255,7 +255,7 @@ doesn't change anything, since the action of \code{UT} on morphisms is
 trivial. So, indeed, the \code{μ} obtained from the adjunction is the
 same as the \code{μ} of the original monad \code{T}.
 
-\subsection{The Kleisli Category}\label{the-kleisli-category}
+\section{The Kleisli Category}\label{the-kleisli-category}
 
 We've seen the Kleisli category before. It's a category constructed from
 another category \emph{C} and a monad \code{T}. We'll call this
@@ -366,7 +366,7 @@ in the same monad \code{T} on \emph{C}. The Kleisli adjunction we've
 just seen is the initial object in this category, and the
 Eilenberg-Moore adjunction is the terminal object.
 
-\subsection{Coalgebras for Comonads}\label{coalgebras-for-comonads}
+\section{Coalgebras for Comonads}\label{coalgebras-for-comonads}
 
 Analogous constructions can be done for any
 \href{https://bartoszmilewski.com/2017/01/02/comonads/}{comonad}
@@ -403,7 +403,7 @@ adjunction reproduces the original comonad as the composite
 Similarly, we can construct a co-Kleisli category with co-Kleisli arrows
 and regenerate the comonad from the corresponding adjunction.
 
-\subsection{Lenses}\label{lenses}
+\section{Lenses}\label{lenses}
 
 Let's go back to our discussion of lenses. A lens can be written as a
 coalgebra:
@@ -514,7 +514,7 @@ gives \code{s} back.
 In other words, a well-behaved lens is indeed a comonad coalgebra for
 the \code{Store} functor.
 
-\subsection{Challenges}\label{challenges}
+\section{Challenges}\label{challenges}
 
 \begin{enumerate}
 \item
@@ -531,7 +531,7 @@ UW ⊣ FW
   Prove that the above adjunction reproduces the original comonad.
 \end{enumerate}
 
-\subsection{Acknowledgment}\label{acknowledgment}
+\section{Acknowledgment}\label{acknowledgment}
 
 I'd like to thank Gershom Bazerman for helpful comments.