small corrections

Author: benediktahrens

tex/CT4P.tex

@@ -12,6 +12,7 @@
 \usepackage{verbatim}
 \usepackage{ccicons}
 \usepackage{enumitem}
+\usepackage{bussproofs}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
@@ -429,14 +430,14 @@ \section{Categories and Examples}
 \end{enumerate}
 \end{dfn}
 
-\begin{intu} So what does a category represent? There are (at least) $3$ possible ways how one can think about this definition:
-\begin{enumerate}
-\item A category represents a type system in the sense that the objects are the types and each hom-set is the type\footnote{In this case, each hom-set is a type, so isn't each hom-set an object again? Categories which satisfy such a property are called \textit{cartesian closed}.} of functions. See \cref{example:hask}.
-\item A category represents a \textit{bag} of instances of a particular mathematical structure (e.g. sets with a notion of addition). The objects are then instances of such a mathematical theory (e.g. $(\mathbb{N},+)$) and the morphisms are structure preserving functions (e.g. functions $f$ which satisfy $f(x+y) = f(x) + f(y)$). See \cref{example:set,example:poset,monoidcategory}.
-\item A category represents a directed graph in the sense that an object is a vertex and a morphism is an edge.
-\item Anything (almost at least) can be seen as a category in some exotic way. 
-\end{enumerate}
-\end{intu}
+% \begin{intu} So what does a category represent? There are (at least) $3$ possible ways how one can think about this definition:
+% \begin{enumerate}
+% \item A category represents a type system in the sense that the objects are the types and each hom-set is the type\footnote{In this case, each hom-set is a type, so isn't each hom-set an object again? Categories which satisfy such a property are called \textit{cartesian closed}.} of functions. See \cref{example:hask}.
+% \item A category represents a \textit{bag} of instances of a particular mathematical structure (e.g. sets with a notion of addition). The objects are then instances of such a mathematical theory (e.g. $(\mathbb{N},+)$) and the morphisms are structure preserving functions (e.g. functions $f$ which satisfy $f(x+y) = f(x) + f(y)$). See \cref{example:set,example:poset,monoidcategory}.
+% \item A category represents a directed graph in the sense that an object is a vertex and a morphism is an edge.
+% \item Anything (almost at least) can be seen as a category in some exotic way. 
+% \end{enumerate}
+% \end{intu}
 
 \begin{nota} Let $\CC$ be a category.
 \begin{itemize}
@@ -832,7 +833,7 @@ \section{Categories and Examples}
     More generally for each field $\mathbb{F}$, one can define $\MAT_\mathbb{F}$, where a morphism $f : m \to n$ is a an $n \times m$ matrix over the field $\mathbb{F}$.
   \end{enumerate}
 
-  Can you think of other categories that have natural numbers as their collection of objects? What about a category, where a morphism $f : m \to n$ is a monotonically increasing (decreasing) function from $[m]$ to $[n]$?
+  Can you think of other categories that have natural numbers as their collection of objects? What about a category, where a morphism $f : m \to n$ is a monotonously increasing (decreasing) function from $[m]$ to $[n]$?
 \end{exer}
 
 \begin{exer}[\cref{sol:category_of_relations}] \label{exer:category_of_relations}
@@ -887,17 +888,20 @@ \section{Isomorphisms}
 \end{exer}
 
 \begin{exer}[\cref{sol:iso_in_sets}]\label{exer:iso_in_sets}
-  Characterize/describe the isomorphisms in $\SET$.
+  Describe the isomorphisms in $\SET$.
 \end{exer}
 
 \begin{exer}[\cref{sol:iso_in_pos}]\label{exer:iso_in_pos}
   Describe the isomorphisms in $\POS$.
 \end{exer}
 
-\begin{exer}[\cref{sol:iso_in_posetcategory}]\label{exer:iso_in_posetcategory} Let $(X,\leq)$ be a poset. Can you characterize/describe the isomorphisms in $\POS(X,\leq)$?
+\begin{exer}[\cref{sol:iso_in_posetcategory}]\label{exer:iso_in_posetcategory}
+  Let $(X,\leq)$ be a poset.
+  Describe the isomorphisms in $\POS(X,\leq)$.
 \end{exer}
 
-\begin{exer} Can you characterize/describe the isomorphisms in $\MON$?
+\begin{exer}
+  Describe the isomorphisms in $\MON$.
 \end{exer}
 
 \begin{exer} Let $\mathcal{G}$ be the category generated by the following graph:
@@ -912,7 +916,7 @@ \section{Isomorphisms}
 \end{exer}
 
 \begin{exer}[\cref{sol:iso_in_posetcategory}] \label{exer:iso_in_cats_of_nats}
-Can you characterize/describe the isomorphisms in $\POS(\NN,\leq)$, $\SKELFINSET$ and $\MAT$?
+  Describe the isomorphisms in $\POS(\NN,\leq)$, $\SKELFINSET$ and $\MAT$.
 \end{exer}
 
 \section{Sections and Retractions}
@@ -1034,10 +1038,10 @@ \section{Monomorphisms and Epimorphisms}
 \end{tikzcd}
 \]
 
-Can you characterize/describe the mono- and epimorphisms in these categories?
+Describe the mono- and epimorphisms in these categories.
 \end{exer}
 
-\begin{exer} Can you characterize/describe the monomorphisms, epimorphisms and isomorphisms in the category generated by the following graph:
+\begin{exer} Describe the monomorphisms, epimorphisms and isomorphisms in the category generated by the following graph:
 \[
 \begin{tikzcd}
 x \arrow[r] & y
@@ -1741,7 +1745,10 @@ \chapter{Functors}\label{sec:functors}
 \end{exer}
 
 
-\begin{exer}\label{ex:poset_functors} Let $(X,\leq_X)$ and $(Y,\leq_Y)$ be preordered sets. Can you characterize/describe the functors from $\PREtoCAT(X,\leq_X)$ to $\PREtoCAT(Y,\leq_Y)$  ? Before writing out the definitions, what would you expect the answer to be?
+\begin{exer}\label{ex:poset_functors}
+  Let $(X,\leq_X)$ and $(Y,\leq_Y)$ be preordered sets.
+  Describe the functors from $\PREtoCAT(X,\leq_X)$ to $\PREtoCAT(Y,\leq_Y)$.
+  Before writing out the definitions, what would you expect the answer to be?
 \end{exer}
 
 \begin{exer}
@@ -1760,7 +1767,9 @@ \chapter{Functors}\label{sec:functors}
 \end{exer}
 
 
-\begin{exer}\label{ex:monoid_functors} Let $(M,m,e)$ be a monoid and let $\MONtoCAT(M,m,e)$ be its corresponding category as defined in \cref{monoidcategory}. Can you characterize/describe the functors from $\MONtoCAT(M,m,e)$ to $\SET$?
+\begin{exer}\label{ex:monoid_functors}
+  Let $(M,m,e)$ be a monoid and let $\MONtoCAT(M,m,e)$ be its corresponding category as defined in \cref{monoidcategory}.
+  Describe the functors from $\MONtoCAT(M,m,e)$ to $\SET$.
 \end{exer}
 
 
@@ -1939,15 +1948,19 @@ \subsection{Functor Categories}
 \end{exer}
 
 \subsection{Exercises}
-\begin{exer} Let $(M,m,e)$ be a monoid and let $\MONtoCAT(M,m,e)$ be its corresponding category. Recall from \cref{ex:monoid_functors} that a functor from $\MONtoCAT(M,m,e)$ to $\SET$ is a set $X$ together with an action of $M$ on $X$, i.e. a function $\mu: M\times X\to X$ such that 
-\[
-\forall x\in X: \mu(e,x) = x, \quad \forall n_1,n_2\in M, x\in X: \mu(n_1, \mu(n_2,x)) = \mu(m(n_1,n_2), x).
-\]
-We will call a set $ X $ with an action of $ M $ on $ X $ an $ M $-set.
-Characterize/describe the natural transformations between $M$-sets.
+\begin{exer}
+  Let $(M,m,e)$ be a monoid and let $\MONtoCAT(M,m,e)$ be its corresponding category. Recall from \cref{ex:monoid_functors} that a functor from $\MONtoCAT(M,m,e)$ to $\SET$ is a set $X$ together with an action of $M$ on $X$, i.e. a function $\mu: M\times X\to X$ such that 
+  \[
+    \forall x\in X: \mu(e,x) = x, \quad \forall n_1,n_2\in M, x\in X: \mu(n_1, \mu(n_2,x)) = \mu(m(n_1,n_2), x).
+  \]
+  We will call a set $ X $ with an action of $ M $ on $ X $ an $ M $-set.
+  Describe the natural transformations between $M$-sets.
 \end{exer}
 
-\begin{exer} Let $(X,\leq_X)$ and $(Y,\leq_Y)$ be posets. Recall from \cref{ex:poset_functors} that a functor between posets corresponds with an order-preserving function, i.e. $x_1 \leq_X x_2 \implies f(x_1) \leq_Y f(x_2)$. Characterize/describe the natural transformations between order-preserving functions.
+\begin{exer}
+  Let $(X,\leq_X)$ and $(Y,\leq_Y)$ be posets.
+  Recall from \cref{ex:poset_functors} that a functor between posets corresponds with an order-preserving function, i.e. $x_1 \leq_X x_2 \implies f(x_1) \leq_Y f(x_2)$.
+  Describe the natural transformations between order-preserving functions.
 \end{exer}
 
 \subsection{Equivalence of Categories}

tex/data.tex

@@ -14,7 +14,13 @@ \section{Examples}
 | $\Zero$ : $\NN$
 | $\Succ$ : $\NN \to \NN$
 \end{lstlisting}
-and the following  category:
+
+  This inductive datatype comes with the following recursion principle:
+
+  
+
+  
+  and the following  category:
   \begin{itemize}
   \item Objects are triples $(X, z \in X, s : X \to X)$ with $X$ a set/type;
   \item Morphisms from $(X, z \in X, s : X \to X)$ to $(X', z' \in X', s' : X' \to X')$ are functions
@@ -214,9 +220,8 @@ \section{Datatypes as Initial Algebras}
 
 
 \begin{exer} 
-Let $F$ be the endofunctor defined as in \cref{example:algebra_of_monoids}, 
-i.e. the endofunctor whose algebras correspond with monoids. 
-Characterize/describe the $F$-algebra homomorphisms.
+  Let $F$ be the endofunctor defined as in \cref{example:algebra_of_monoids}, i.e., the endofunctor whose algebras correspond to monoids. 
+  Describe the $F$-algebra homomorphisms.
 \end{exer}
 
 \begin{dfn}\label{definition:category_of_Falgebras} Let $F:\CC\to \CC$ be an endofunctor. The \textbf{category of $F$-algebras}, denoted by $\ALG{F}$, is defined by the following data:
@@ -280,25 +285,25 @@ \section{Datatypes as Initial Algebras}
 \end{exer}
 
 \begin{exer}\label{exer:bool_as_initial_algebra}
- Let $\mathbf{Bool}$ be the inductive data type generated by the following two constructors:
- \begin{lstlisting}
+  Let $\mathbf{Bool}$ be the inductive data type generated by the following two constructors:
+\begin{lstlisting}
     True  : Bool
     False : Bool
-  \end{lstlisting}
- Define an endofunctor $F:\SET\to \SET$ such that the $F$-algebras can be characterized as triples $(X, b_1, b_2)$ with $X$ a set and $b_1,b_2\in X$.
- 
-Moreover, show that $(\mathsf{Bool}, \mathsf{True}, \mathsf{False})$ is an initial object in $\ALG{F}$.
+\end{lstlisting}
+  Define an endofunctor $F:\SET\to \SET$ such that the $F$-algebras can be described as triples $(X, b_1, b_2)$ with $X$ a set and $b_1,b_2\in X$.
+  
+  Moreover, show that $(\mathsf{Bool}, \mathsf{True}, \mathsf{False})$ is an initial object in $\ALG{F}$.
 \end{exer}
 
 \begin{exer}\label{exer:coproduct_as_initial_algebra}
-The disjoint union (i.e., the coproduct) of two sets $X$ and $Y$ can also be characterized as an inductive data type; indeed, it is generated by the following two constructors:
- \begin{lstlisting}
+  The disjoint union (i.e., the coproduct) of two sets $X$ and $Y$ can also be described as an inductive data type; indeed, it is generated by the following two constructors:
+\begin{lstlisting}
     f : X -> X+Y
     g : Y -> X+Y
-  \end{lstlisting}
-Define an endofunctor $F:\SET\to \SET$ such that the $F$-algebras can be characterized as triples $(C, i_l, i_r)$ with $C$ a set and $i_l : X\to C, i_r : Y\to C$ be functions.
+\end{lstlisting}
+  Define an endofunctor $F:\SET\to \SET$ such that the $F$-algebras can be described as triples $(C, i_l, i_r)$ with $C$ a set and $i_l : X\to C, i_r : Y\to C$ be functions.
 
-Moreover, show that $(X + Y, \inl, \inr)$ is the initial object in $\ALG{F}$, where $X+Y$ is the disjoint union of $X$ and $Y$ (i.e. the coproduct in $\SET$) and $\inl:X\to X+Y, \inr:Y\to X+Y$ the canonical inclusions.
+  Moreover, show that $(X + Y, \inl, \inr)$ is the initial object in $\ALG{F}$, where $X+Y$ is the disjoint union of $X$ and $Y$ (i.e. the coproduct in $\SET$) and $\inl:X\to X+Y, \inr:Y\to X+Y$ the canonical inclusions.
 \end{exer}
 
 \begin{exer}\label{exer:conatural_numbers_are_not_initial}