cats.tex

\chapter{A categorical interlude}
\label{ch:cats}
\marginnote{%
  This chapter introduces some useful terminology that we'll use in the rest of the book.
  It can probably be skipped at a first reading, and only consulted as needed.}

We have seen that many types carry a notion of morphism between its elements:
\begin{itemize}
\item We have functions $f : A \to B$ between types $A$ and $B$ in a universe $\UU$
  (\cref{univalent-mathematics}),
\item We have identifications $p : x \eqto y$ between elements $x,y$ of any type $A$
  (\cref{sec:identity-types}),
\item We have pointed functions $f : A \ptdto B$ between pointed types $A$ and $B$ in $\UUp$
  (\cref{def:pointedtypes}),
\item We have fiberwise maps $f : \prod_{x:X}(A(x) \to B(x))$ between families $A,B : X \to \UU$ (\cref{def:fiberwise}),
\item We have homomorphisms $f : \Hom(G, H)$ between groups $G, H : \Group$
  (\cref{def:grouphomomorphism}),
\wip{\item We have maps of cycles $f : (X,t) \to (Y,u)$ and of bicycles $(X,a,b) \to (X',a',b')$,}
\item We have maps of $G$-sets $f : \Hom_G(X,Y)$ for $X,Y : \BG \to \Set$
  (\cref{def:map-of-Gsets}; a special case of fiberwise maps).
\end{itemize}
In all those cases, we have notions of identity morphism and composition of morphisms.
We have also seen that some maps between types are paired with maps on morphisms, for example,
taking underlying symmetries in groups, $\USym : \Group \to \Set$ (\cref{def:group-symmetries}),
comes with a corresponding operation of taking the underlying map of symmetries of a group homomorphism,
\[ \USym : \Hom(G,H) \to (\USymG \to \USymH) \]
(\cref{def:USym-hom}) satisfying $\USym(\id_G) = \id_{\USymG}$ and $\USym(\psi\circ\varphi) = \USym\psi \circ \USym\varphi$ (\cref{cor:USym-compose}).

It's very useful to develop some abstractions for types equipped with a notion of morphism and maps equipped with maps of morphisms like this.
These give the notions of (wild) \emph{categories} and \emph{functors}, respectively,
and \emph{category theory} is the study of these structures.

Here we give a brief primer\footnote{%
  The topic is of course too vast to cover in detail here,
  so we refer to the literature for more details.
  Category theory in univalent foundations is also treated in
  Chapter~10 of the HoTT book\footnotemark{}
  (based on~\citeauthor{AKS2015}\footnotemark{}),
  while \citeauthor{AwodeyCat}\footnotemark{}
  and \citeauthor{RiehlContext}\footnotemark{}
  give traditional expositions,
  and \citeauthor{MacLaneWorking}\footnotemark{}
  gives a comprehensive treatment.}%
\addtocounter{footnote}{-3}\footcitetext{hottbook}%
\stepcounter{footnote}\footcitetext{AKS2015}%
\stepcounter{footnote}\footcitetext{AwodeyCat}%
\stepcounter{footnote}\footcitetext{RiehlContext}%
\stepcounter{footnote}\footcitetext{MacLaneWorking}%
on category in order to systematize what we've done so far,
and prepare for the main result of the next chapter, which is to give an
\emph{equivalence of categories} between the categories of concrete and abstract groups.

\section{Brief overview of the chapter}

In~\cref{sec:categories} we define the kinds of categories we need, along with many examples (including the above).
Then we discuss various abstract notions in categories (terminal and initial objects, products and coproducts)
and remark on the importance of \emph{duality} in~\cref{sec:duality}.
In~\cref{sec:naturality} we cover functors and natural transformations,
and in~\cref{sec:adjunctions} we treat adjunctions;
we have already seen some examples of adjunctions,
for example in~\cref{xca:adjunction-_!-^*,xca:adjunction-^*-_*}.

We have also seen an incarnation of the Yoneda lemma in~\cref{xca:TTYoneda};
in~\cref{sec:yoneda} we treat the O.G.\ version. We end with a brief introduction to monoidal categories in~\cref{sec:monoidal-cats}, as we'll see in~\cref{ch:abelian} that abelian groups form an example.

\section{Categories}
\label{sec:categories}

As mentioned above, many types come equipped with notion
of \emph{morphism} or \emph{arrow} between its elements
which is more general than identification or \emph{isomorphism}.
For instance
we have type of functions $A \to B$ for $A,B:\UU$
and the type of pointed functions $A \ptdto B$ for $A,B:\UUp$.
There are identity morphisms and composition of morphisms,
and this motivates the following definition:

\begin{definition}\label{def:wild-cat}
  A \emph{wild precategory}\index{category!wild precategory}\footnote{%
    See below for remarks on the terminology.
    Adding further properties to the data given here eventually
    recovers the notion of a category \emph{simpliciter},
    see \cref{def:category}.}
  consists of the following data:
  \begin{enumerate}
  \item\label{struc:cat-ob} A type $\var{Ob}$, called the \emph{type of objects}.
  \item\label{struc:cat-mor} For each pair of objects $A,B : \var{Ob}$,
    a type of \emph{morphisms} $\hom(A,B)$. These are also known as \emph{arrows},
    and written $A \to B$ when there's no danger of confusion.
    If $f : A \to B$ is such an arrow, then we say that the \emph{domain} of $f$ is $A$
    and the \emph{codomain} of $f$ is $B$.
  \item\label{struc:cat-id} For each object $A : \var{Ob}$,
    an \emph{identity arrow} $\id_A : A \to A$.
  \item\label{struc:cat-comp} For each pair of arrows $f : A \to B$ and $g : B \to C$,
    a \emph{composite arrow} $g\circ f : A \to C$.\footnote{%
      To be fully explicit, the composition operation has
      type
      \[
        \prod_{A,B,C:\var{Ob}}(B \to C) \to (A \to B) \to (A \to C),
      \]
      and we might denote it $g \circ_{A,B,C} f$.
      Since the objects $A$, $B$, and $C$ can often be inferred,
      we leave them out, lest the notation becomes too heavy.
      A similar remark goes for the other operations.}
  \item\label{struc:cat-unit-laws} For each arrow $f : A \to B$,
    a pair of identifications
    \[
      \lambda : \id_B \circ f \eqto f, \quad
      \rho : f \circ \id_A \eqto f.
    \]
  \item\label{struct:cat-assoc} For each triple of arrows
    $f : A \to B$, $g : B \to C$, and $h : C \to D$, an identification
    \[
      \alpha : h \circ (g \circ f) \eqto (h \circ g) \circ f.
    \]
  \end{enumerate}
  If $\mathcal C \jdeq (\var{Ob},\hom,\id,\lambda,\rho,\alpha)$
  is a wild precategory, then we write $A, B : \mathcal C$ instead of $A, B : \var{Ob}$
  to indicate that $A, B$ are elements of the underlying type of objects of $\mathcal C$.
  We also write $\constant{Ob}(\mathcal C)$ for this type.
  We may write $f, g : A \to_{\mathcal C} B$ to emphasize where the arrows $f$ and $g$ live, if needed,
  and sometimes $\hom_{\mathcal C}(A,B)$ or $\mathcal C(A,B)$, instead of $\hom(A,B)$.
\end{definition}
\begin{remark}[On the adjective ``wild'']
  With this definition, we readily equip the universes of types $\UU$ and of pointed types $\UUp$
  with a structure of wild precategories.
  In the former case, we can use reflexivities for $\lambda$, $\rho$, and $\alpha$.
  In the latter, we leave their definition as an exercise.

  We use the adjective ``wild'' to highlight a deficiency of this definition as it stands:
  We haven't specified any further laws for the identifications $\lambda$, $\rho$, and $\alpha$.
  For example, it would be sensible to require an identification of $\lambda$ and $\rho$ at an identity:
  $\id_A \circ \id_A \eqto \id_A$,
  as well as a filler for the pentagonal diagram of $\alpha$'s coming from four composable arrows:
  \begin{equation}\label{eq:pentagon}
    \begin{tikzpicture}[commutative diagrams/every diagram]
      \node (P0) at (90:2.3cm) {$k \circ (h \circ (g \circ f))$};
      \node (P1) at (90+72:2cm) {$k \circ ((h \circ g) \circ f)$};
      \node (P2) at (90+2*72:2cm) {\makebox[5ex][r]{$(k \circ (h \circ g)) \circ f$}};
      \node (P3) at (90+3*72:2cm) {\makebox[5ex][l]{$((k \circ h) \circ g) \circ f$}};
      \node (P4) at (90+4*72:2cm) {$(k \circ h) \circ (g \circ f)$};
      \path[commutative diagrams/.cd, every arrow, every label]
      (P0) edge[eql] node[swap] {$\ap{k\circ\blank}(\alpha)$} (P1)
      (P1) edge[eql] node[swap] {$\alpha$} (P2)
      (P2) edge[eql] node[swap] {$\ap{\blank\circ f}(\alpha)$} (P3)
      (P4) edge[eqr] node {$\alpha$} (P3)
      (P0) edge[eqr] node {$\alpha$} (P4);
    \end{tikzpicture}
  \end{equation}
  Of course, we would on occasion then need a filler for a three dimensional diagram of pentagons
  for five composable arrows, etc., etc., \emph{ad infinitum}.\footnote{%
    There is a hierarchy of notions, $A_n$-precategories, for $n\ge 2$,
    with coherence conditions involving up to $n$ composable arrows.
    The wild precategories lie between $A_2$ and $A_3$ in this hierarchy.
    Besides the mentioned identification of $\lambda$ and $\rho$ for two identities,
    we'd also require fillers for diagrams like
    \[
      \begin{tikzcd}[ampersand replacement=\&,column sep=tiny]
        \& f\circ g \& \\
        f\circ(\id\circ g) \ar[rr,eql,"\alpha"']\ar[ur,eqr,"{\ap{f\circ\blank}(\lambda)}"]
        \& \& (f\circ\id)\circ g\ar[ul,eql,"{\ap{\blank\circ g}(\rho)}"']
      \end{tikzcd}
    \]
    as well as coherences when one or both of $f$ and $g$ are identities.}
  The corresponding structure is known to connoisseurs as an $(\infty,1)$-precategory.
  It is an open problem as we write this whether this notion can be defined in our type theory.
  We would certainly hope that types and pointed types would furnish examples.
\end{remark}

However, when the types of morphisms $\hom(A,B)$ are \emph{sets}, then the types
of $\lambda$, $\rho$, and $\alpha$ are propositions, so any coherence conditions
are automatically fulfilled.
This motivates the following definition.

\begin{definition}\label{def:precategory}
  A \emph{precategory}\index{category!precategory}
  is a wild precategory $\mathcal C$ in which the types
  $A \to_{\mathcal C} B$ are sets, for all objects $A,B : \mathcal C$.
\end{definition}

Most (wild) precategories we shall meet satisfy a further condition
that makes them better behaved than arbitrary precategories:
a \emph{univalence} condition.
In fact, for the wild precategory of types and functions,
this condition is exactly the Univalence Axiom (\cref{def:univalence})!

In order to define this, we need the notion corresponding to equivalence
in an general wild precategory.

\begin{definition}
  A morphism $f : A \to B$ in a wild precategory $\mathcal{C}$ is an
  \emph{isomorphism}\index{isomorphism!in a (wild pre-)category}
  if have $g, h : B \to A$ and identifications
  $\sigma : \id_B \eqto f\circ g$ and $\rho : \id_A \eqto h\circ f$.
  This condition is encoded by the type
  \[
    \isIso(f) \defeq \biggl(\sum_{g:B\to A}f\circ g\eqto\id_B\biggr)
    \times\biggl(\sum_{h:B\to A}h\circ f\eqto\id_A\biggr)
  \]
  If $f$ is an isomorphism, we also say that $f$ is \emph{invertible}.

  We define the type $A \isoto B$ of \emph{isomorphisms} from $A$ to $B$
  in $\mathcal C$ ($A \isoto_{\mathcal C} B$ if needed)
  by the following definition.%
  \glossary(2isoto){$\protect\isoto$}{type of isomorphisms}
  \[
    (A \isoto B) \defeq \sum_{f:A\to B} \isIso(f).\qedhere
  \]
\end{definition}
The type $\isIso(f)$
is indeed a proposition,\footnote{%
  This follows just as for functions: If $f$ is an isomorphism,
  then each factor in the product is contractible, as, e.g.,
  $\sum_{g:B\to A}f\circ g\eqto\id_B$ is the fiber
  of $f\circ\blank : (B \to A) \to (B \to B)$
  at $\id_B$, and all functions $f\circ\blank$ and $\blank\circ f$
  are equivalences of types using the data that makes $f$ an isomorphism
  along with $\lambda$, $\rho$, and $\alpha$.}
and every identity arrow is an isomorphism.
We write $\inv f$ for the inverse of an isomorphism $f$.
\begin{definition}
  A wild precategory $\mathcal C$ is \emph{univalent}\index{univalent} if
  for all objects $A,B : \constant{Ob}(\mathcal C)$, the function
  \[
    \constant{idtoiso}_{A,B} : (A \eqto_{\constant{Ob}(\mathcal C)} B) \to (A \isoto_{\mathcal C} B)
  \]
  defined by path induction sending $\refl A$ to $\id_A$,
  is an equivalence.
\end{definition}
\begin{definition}\label{def:category}
  A \emph{wild category}\index{category!wild category} is a univalent wild precategory,
  and a \emph{category}\index{category} is a univalent precategory.
\end{definition}
Now we are ready to restate the examples mentioned in the introduction to the chapter.
In each case we leave it to the reader to supply most of the data.
\begin{itemize}
\item
  The \emph{wild category of types} (in universe $\UU$) has $\UU$
  as its type of objects, and the function type $A \to B$ as its type of arrows
  for $A,B :\UU$. It is univalent by the Univalence Axiom.
\item
  The \emph{wild category of pointed types} (in a universe $\UU$) has
  $\UUp$ as its type of objects, and the type of pointed maps $A \ptdto B$ as its type of arrows.
\item
  The \emph{wild category of families} over a given type $X$ has
  $X \to \UU$ as its type of objects, and the type of fiberwise maps
  $(X \to_B Y) \defeq \prod_{b:B}X(b) \to Y(b)$
  as its type of arrows.
\item
  The \emph{category of sets}\index{category!of sets} has $\Set$
  as its type of objects, and the function type $A \to B$ as its type of arrows.
  It's a category since each type $A\to B$ is a set, and it's univalent.
\item
  The \emph{category of groups}\index{category!of groups} has $\Group$
  as its type of objects, and the homomorphism type $(G \to H) \defeq \Hom(G,H)$
  as its type of arrows.
\item
  The \emph{category of $G$-sets}\index{category!of $G$-sets}, for a group $G$,
  has $\GSet$ as its type of objects, and the type of morphisms of $G$-sets
  $\Hom_G(X,Y)$ (\cref{def:map-of-Gsets}) as its type of arrows.
\end{itemize}

By the univalence condition, in a category each identity type $A \eqto B$
is equivalent to the set $A \isoto B$, and is hence a set.
Thus we get the following.
\begin{lemma}
  The type of objects of a category form a groupoid.
\end{lemma}

And important special case is when each arrow type $A \to B$ is a \emph{proposition}.
\begin{example}\label{ex:poset}
  A \emph{preorder}\index{preorder} is precategory in which every arrow type is a proposition.
  In this case, the types of $\lambda$, $\rho$, and $\alpha$ are contractible, so the data
  of a preorder reduces to just a type $P$ and a binary relation,
  typically written $\le : P \to P \to \Prop$,
  that is reflexive, $x \le x$ (via the identities)
  and transitive, \ie if $x\le y$ and $y\le z$ implies $x\le z$ (via composition).

  A \emph{partial order}\index{partial order}, also known as a \emph{poset}\index{poset},
  is a univalent preorder.
  In this case, the type of objects is a set.
  This happens if and only if the relation is symmetric,
  \ie if $x \le y$ and $y \le x$ implies $x = y$.

  Typical examples are $(\NN,\le)$, $(\ZZ,\le)$, $(\Prop,\to)$,
  and $(\Sub(S),\subseteq)$ for a set $S$.
  A preorder that fails to be a poset is the two-element type $\bn 2$
  with the always true relation.
  This is hence also an example of a precategory that fails to be univalent.
\end{example}

Another important special case is when every morphism is an isomorphism.
\begin{definition}\label{def:wild-pre-groupoid}
  A (\emph{wild}) \emph{pregroupoid} is a (wild) precategory in which every
  arrow is invertible.
  A (\emph{wild}) \emph{groupoid} is a univalent (wild) pregroupoid.
\end{definition}
\begin{example}
  Every type $X$ gives rise to a wild groupoid, its (wild) \emph{path groupoid},
  having $X$ as its type of objects and $x \eqto y$ as its type of arrows.
  The arrows are invertible, since paths are always invertible.

  If $X$ is a $1$-type, then this structure is a groupoid.
\end{example}
There's no conflict with the terminology introduced in~\cref{sec:props-sets-grpds},
because this construction gives an equivalence
from the type of $1$-types (in $\UU$) to the type of groupoids (in $\UU$),
as we shall see below.

\Cref{def:wild-cat,def:precategory,def:category,def:wild-pre-groupoid}
are summarized as a diagram of inclusions in~\cref{fig:cat-summary}.

\begin{figure}
\begin{sidecaption}%
  {The various notions of categories arranged in a cube: on the bottom face
    we loose the adjective ``wild'' by requiring arrows to form \emph{sets};
    on the front left face we loose the prefix ``pre'' by requiring
    \emph{univalence}; and on the front right face we restrict to groupoids by
    requiring all arrows be \emph{invertible}.}[fig:cat-summary]
  \centering
  \footnotesize
  \begin{tikzpicture}
    \node (wpc) at (0,3) {wild precategory};
    \node (wc) at (-3,1) {wild category};
    \node (wpg) at (3,1) {wild pregroupoid};
    \node (wg) at (0,-1) {wild groupoid};
    \node (pc) at (0,1) {precategory};
    \node (c) at (-3,-1) {category};
    \node (pg) at (3,-1) {pregroupoid};
    \node (g) at (0,-3) {groupoid};
    \begin{scope}[->,commutative diagrams/hook]
      \draw (g) -- (pg);
      \draw (g) -- (c);
      \draw (pg) -- (pc);
      \draw (c) -- (pc);
      \draw (pc) -- (wpc);
      \draw (wc) -- (wpc);
      \draw (wpg) -- (wpc);
      \draw[commutative diagrams/crossing over] (wg) -- (wc);
      \draw[commutative diagrams/crossing over] (wg) -- (wpg);
      \draw (c) -- (wc);
      \draw (g) -- (wg);
      \draw (pg) -- (wpg);
    \end{scope}
    \node at (-4,-.5) [casred]{hom-\emph{sets}};
    \node at (-2,-2.5) [casred]{%
      \begin{tabular}{c}only \\ \emph{iso}morphisms\end{tabular}};
    \node at (2,-2.5) [casred]{\emph{univalence}};
  \end{tikzpicture}
\end{sidecaption}
\end{figure}

\begin{remark}
  This is a good moment to remark on the size issues
  we have so far swept under the rug.
  The definition of a wild precategory $\mathcal C$ can be parametrized by
  \emph{two} universe levels: The type of objects belong to one, $\var{Ob}:\UU'$,
  while the family of arrows belong to another, $\hom : \var{Ob} \to \var{Ob} \to \UU$.

  If they coincide, then we call $\mathcal C$ a \emph{$\UU$-small category}\index{category!small}.
  For instance, a path groupoid for a type $X:\UU$ is $\UU$-small.

  The other common case is where $\UU:\UU'$, in which case
  we call $\mathcal C$ \emph{locally $\UU$-small}\index{category!locally small}.
  For example, the (wild) categories of types, sets, pointed types, groups, etc., built
  from types in $\UU$ are all locally $\UU$-small.
  This generalizes~\cref{def:ess-loc-small} for the case of path groupoids.
\end{remark}

Many notions in category theory work already at the level of wild categories,\footnote{%
  They \emph{all} work at the level of $(\infty,1)$-categories.
  We refer to \citeauthor{LurieHTT}\footnotemark{} and
  \citeauthor{LandInftyCat}\footnotemark{} for details.}%
\addtocounter{footnote}{-1}\footcitetext{LurieHTT}%
\stepcounter{footnote}\footcitetext{LandInftyCat}
but a notable exception is the construction of slice categories,
(also known as \emph{over categories}).
\begin{example}\label{def:slice-cat}
  The \emph{slice precategory} of a precategory $\mathcal C$ over an object $C : \mathcal{C}$,
  denoted $\mathcal C/C$,
  has as objects the type $\sum_{A:\mathcal C}A \to C$ of pairs $(A,f)$ of an object $A$ and an arrow $f:A\to C$
  with codomain $C$.
  An arrow from $(A,f)$ to $(A',f')$ is an arrow $g : A \to A'$ such that $f' \circ g=f$.\footnote{%
    This is a proposition since $\mathcal C$ is a precategory. We illustrate the arrow as
    a commuting triangle:
    \[
      \begin{tikzcd}[ampersand replacement=\&,column sep=small]
        A \ar[dr,"f"']\ar[rr,"g"] \& \& A' \ar[dl,"f'"] \\
        \& C \&
      \end{tikzcd}
    \]}
  The identities and compositions are inherited from $\mathcal C$.
  If $\mathcal C$ is univalent (and hence a category), then so is $\mathcal C/C$.

  If we try to define the slice $\mathcal C/C$ for an arbitrary wild precategory $\mathcal C$,
  using identifications $f' \circ g \eqto f$, we find that we need the pentagon coherence
  for $\alpha$ for $\mathcal C$ in order to define the $\alpha$ for $\mathcal C/C$.

  Of course, for \emph{particular} wild categories, it may very well happen
  that $\mathcal C/C$ is again a wild categories.\footnote{%
    This will be the case when $\mathcal C$ should be an $(\infty,1)$-category,
    carrying the whole hierarchy of coherences, which then
    carry over to $\mathcal C/C$.}
\end{example}
\begin{xca}\label{xca:univ-slice-cat}
  Construct a wild precategory structure on the \emph{slice of the universe} $\UU/B$
  over a fixed type $B:\UU$.
\end{xca}

\section{Abstract notions and duality}
\label{sec:duality}

Many concepts that we introduced in~\cref{ch:univalent-mathematics}
for the wild category of types make sense in arbitrary wild precategories.

\begin{definition}
  A \emph{terminal object}\index{terminal object}
  in a wild precategory $\mathcal C$ is an object $1$
  such that for any object $A:\mathcal C$,
  the arrow type $A \to 1$ is contractible.
\end{definition}
\begin{xca}
  Show that if $\mathcal C$ is univalent, then
  the type of terminal objects is a proposition.
\end{xca}
The unit type $\bn 1$ is a terminal object in the wild category of types,
and in the category of sets,
while the trivial group $\TG$ is a terminal object in the category groups.

The is a ``dual'' notion as well.
\begin{definition}
  An \emph{initial object}\index{initial object}
  in a wild precategory $\mathcal C$ is an object $0$
  such that for any object $A:\mathcal C$,
  the arrow type $0\to A$ is contractible.
\end{definition}
For example, the empty type $\bn 0$ is initial in the wild category of types,
while the trivial group $\TG$ is initial in the category of groups.

The relationship between terminal and initial objects reflects
a deep aspect of category theory: Every concept comes with a dual version
obtained by ``reversing all the arrows''.
More formally, can introduce for every wild precategory its opposite category
that has its arrows reversed.
\begin{definition}
  For any wild precategory $\mathcal C\jdeq(\var{Ob},\hom,\id,\lambda,\rho,\alpha)$,
  define the \emph{opposite}\index{category!opposite} $\mathcal C\op$
  to have the same type of objects,
  morphisms $\hom_{\mathcal C\op}(A,B) \defeq \hom_{\mathcal C}(B,A)$,
  identities the same, and composition reversed:
  If $f : A \to_{\mathcal C} B$ and $g : B \to_{\mathcal C} C$,
  then $g\circ f : A \to_{\mathcal C} C$ works
  as the composite $f \circ_{\mathcal C\op} g$ of $g : C \to_{\mathcal C\op} B$
  and $f : B \to_{\mathcal C\op} A$.
  We then swap the roles of $\lambda$ and $\rho$,
  and $\inv\alpha$ plays the role of $\alpha$ in $\mathcal C\op$.
\end{definition}
\begin{lemma}
  The operation of taking opposites defines an equivalence
  from the type of wild precategories to itself,
  with a trivially defined identification $(\mathcal C\op)\op \eqto C$.
\end{lemma}
It follows that any construction or theorem about wild precategories
has a dual version, obtained by precomposition with $(\blank)\op$.

For example, the dual of the slice category construction
is the \emph{coslice} category $C/\mathcal C$
(also known as the \emph{under category}).

As a further example of a pair dual notions, we consider that of
monomorphisms and epimorphisms.
\begin{definition}
  An arrow $f : A \to B$ in a wild precategory $\mathcal C$
  is called a \emph{monomorphism}\footnote{For short: a mono} if
  post-composition with $f$ is an injection
  \[
    f\circ\blank : (C \to_{\mathcal C} A) \to (C \to_{\mathcal C} B)
  \]
  for all objects $C:\mathcal C$.

  Dually, $f$ is called an \emph{epimorphism}\footnote{For short: an epi}
  if pre-composition with $f$ is an injection
  \[
    \blank\circ f : (B \to_{\mathcal C} C) \to (A \to_{\mathcal C} C)
  \]
  for all objects $C:\mathcal C$.\footnote{%
    We can illustrate these in diagrams as saying that
    $f$ is a mono if a map into the codomain of $f$ factors in
    at most one way through the domain of $f$,
    \[
      \begin{tikzcd}[ampersand replacement=\&,column sep=small]
        \& A \ar[d,"f"] \\
        C \ar[ur,dashed]\ar[r] \& B
      \end{tikzcd}
    \]
    and dually, $f$ is an epi if a map out of the domain of $f$
    factors in at most one way through the codomain of $f$:
    \[
      \begin{tikzcd}[ampersand replacement=\&,column sep=small]
        A \ar[d,"f"']\ar[r] \& C \\
        B \ar[ur,dashed]
      \end{tikzcd}
    \]}
  If $C$ is a precategory, then these conditions reduce to the implications
  \[
    f\circ g=f\circ h \to g=h, \quad\text{and}\quad g\circ f=h\circ f \to g=h,
  \]
  respectively.
\end{definition}
We already met the monomorphisms in the category of groups in~\cref{def:typeofmono}
using a different definition.
\begin{xca}
  Show that the monomorphisms in the category of groups are the same as
  those of~\cref{def:typeofmono}.
\end{xca}
\begin{xca}
  Show that the monomorphisms in the wild category of types are just the injections,
  and the epimorphisms in the category of sets are just the surjections.
\end{xca}
The epimorphisms in the wild category of types are always surjections,
but are much more restricted. See~\citeauthor{BdJR2025}\footcite{BdJR2025} for details.
\begin{xca}
  Show that every morphism in a preorder is both a mono and an epi.
\end{xca}

\section{Functors and natural transformations}
\label{sec:naturality}

Not only do have arrows \emph{in} (wild pre-)categories, there's also
a notion of arrow \emph{between} them. These are called functors.
\begin{definition}\label{def:functor}
  A \emph{wild functor}\index{functor}
  $F : \mathcal C \to \mathcal D$
  between wild precategories $\mathcal C$ and $\mathcal D$
  consists of a function
  $F : \constant{Ob}(\mathcal C) \to \constant{Ob}(\mathcal C)$,
  mapping objects to objects,
  and a family of functions\footnote{%
    In practice, the functions on objects and arrows are named the same as
    the functor, but they could be disambiguated with subscripts,
    say, $F_0$ and $F_1$, if needed.}
  \[
    F : \prod_{A,B:\mathcal C}(A \to_{\mathcal C} B) \to (F(A) \to_{\mathcal D} F(B))
  \]
  together with identifications
  \[
    F_{\id} : F(\id_A) \eqto \id_A,\quad\text{and}\quad
    F_{\circ} : F(g\circ f) \eqto F(g)\circ F(f),
  \]
  for all objects $A$ and composable arrows $f$ and $g$ in $\mathcal C$.

  If $\mathcal D$ is a precategory, then the types of $F_{\id}$ and $F_{\circ}$
  are propositions, and in this case we just call $F$ a \emph{functor}.
\end{definition}
\begin{xca}
  Show that every wild functor maps isomorphisms to isomorphisms.
\end{xca}
\begin{example}
  A functor between preorders $(P,\le)$ and $(Q,\le)$ amounts to a monotone map
  $F : P\to Q$, \ie $p\le p'$ implies $F(p) \le F(p')$ for $p,p':P$.
\end{example}
\begin{example}
  Taking the underlying set of symmetries $\USym$
  gives a functor $\USym : \Group \to \Set$.
  It's easy to check that $\USym(\id_G) = \id_{\USymG}$,
  and we verified the preservation of composition
  in~\cref{cor:USym-compose}.
\end{example}
\begin{example}
  Given a group homomorphism $f : G \to H$,
  we have three functors
  \[
    \begin{tikzcd}
      \GSet[G] \ar[r,bend left,"f_!"]\ar[r,bend right,"f_*"'] &
      \GSet[H] \ar[l,"f^*"' description]
    \end{tikzcd}
  \]
  with actions on objects described in~\cref{def:restrictandinduce,rem:coinduced-Hset}.
  The action on arrows of restriction is again given by restriction:
  If $g : X \to Y$ is a map of $H$-sets with $X,Y:\BH \to \Set$,
  then $f^*(g) : f^*X \to f^*Y$ maps $z:\BG$ to $g_{\Bf(z)} : X(\Bf(z)) \to Y(\Bf(z))$.

  The action on arrows of induction along $f$ takes a map of $G$-sets $g : X \to Y$,
  for $X,Y : \BG\to\Set$,
  to the functorial action of set truncation, for $w:\BH$:
\end{example}
\begin{example}\label{def:n-trunc-functor}
  Taking $n$-truncation gives a wild functor
  $\Trunc\blank_n : \UU \to \UU^{\le n}$.
  For $n=0$, this is a functor from $\UU$ to $\Set_\UU$.
\end{example}
\begin{example}\label{ex:add-remove-basepoint}
  We can extend the operation of adding a default element
  from~\cref{def:pointedtypes}
  to a wild functor $(\blank)_+ : \UU \to \UUp$.
  It takes a function $f : A \to B$
  to the function $f_+ : A_+ \to B_+$
  with
  \[
    f_+(\inl a) \defeq \inl{f(a)},\quad\text{and}\quad
    f_+(\pt_{A_+}) \defeq \pt_{B_+}.
  \]
  The operation of taking underlying types of pointed types
  likewise extends to a wild functor $(\blank)_\div : \UUp \to \UU$.
\end{example}
\begin{example}
  Taking loop types extends to a wild functor $\Omega : \UUp \to \UUp$.
  We defined the action on maps in~\cref{def:loops-map},
  except we didn't equip $\Omega k$ with a pointing path, for $k : X \ptdto Y$.
  However, that's easily remedied using the path groupoids
  laws from back in~\cref{xca:path-groupoid-laws}:
  \[
    \pt_{\Omega Y} \jdeq \refl{\pt_Y}
    \eqto \inv{k_\pt} \cdot \refl{k(\pt_X)} \cdot k_\pt
    \jdeq \inv{k_\pt} \cdot \ap{k_\div}(\pt_{\Omega X}) \cdot k_\pt
    \jdeq \Omega k(\pt_{\Omega X})
  \]
  We leave it to the reader to fill in the remaining data.
\end{example}
\begin{example}
  For an object $C$ of a precategory $\mathcal C$,
  recall the slice precategory
  $\mathcal C/C$ of~\cref{def:slice-cat}.
  Taking the domain of an object $(A,f:A\to C)$ of the slice
  extends to a functor $\fst : \mathcal C/C \to \mathcal C$.
\end{example}
\begin{example}
  Similar to the slice and coslice constructions,
  we have the formation of the \emph{arrow precategory} $\mathcal C^\to$
  of a precategory $\mathcal C$.
  It has as objects triples $(A,B,f)$ of two objects $A,B:\mathcal C$
  and an arrow $f: A\to B$.
  The arrows from $(A,B,f)$ to $(A',B',f')$ are pairs of arrows
  $g : A \to A'$ and $h : B\to B'$ making a commutative square:
  \[
    \begin{tikzcd}
      A \ar[d,"f"']\ar[r,"g"] & A'\ar[d,"f'"] \\
      B \ar[r,"h"'] & B'
    \end{tikzcd}
  \]
  Projecting out the domain and the codomain gives
  two functors
  \[
    \begin{tikzcd}
      \mathcal C & \mathcal C^\to \ar[l,"\dom"']\ar[r,"\cod"] & \mathcal C
    \end{tikzcd}
  \]
  Note that $\mathcal C^\to$ is a category if $\mathcal C$ is.
\end{example}
\begin{xca}
  Define identity wild functors and composition of wild functors,
  along with identifications $\lambda : \id_{\mathcal D}\circ F \eqto F$,
  $\rho : F \circ \id_{\mathcal C} \eqto F$,
  and $\alpha : H\circ (G \circ F) \eqto (H \circ G)\circ F$.
  Define the fillers for the pentagon diagram~\eqref{eq:pentagon}
  for four composable functors
  \[
    \mathcal C_0 \xrightarrow F
    \mathcal C_1 \xrightarrow G
    \mathcal C_2 \xrightarrow H
    \mathcal C_3 \xrightarrow K
    \mathcal C_4
  \]
  in the case where $\mathcal C_4$ is a (non-wild) precategory.
\end{xca}
There's also a notion of arrow \emph{between functors}.
These are called natural transformations.\footnote{%
  \citeauthor{Freyd1964}\footnotemark{} observed that ``categories are what one must define
  in order to define functors, and that functors are what one must define
  in order to define natural transformations.''
  In this sense, natural transformations are at the heart of category theory.}%
\footcitetext{Freyd1964}
\begin{definition}
  A \emph{wild natural transformation}\index{natural transformation}
  $\alpha : F \to G$ between
  two wild functors $F,G : \mathcal C \to \mathcal D$ between
  wild precategories $\mathcal C$ and $\mathcal D$
  consists of a family of arrows
  \[
    \alpha_A : F(A) \to_{\mathcal D} G(A)
  \]
  indexed by objects $A:\mathcal C$,
  and a family of fillers for the squares
  \[
    \begin{tikzcd}
      F(A) \ar[r,"\alpha_A"]\ar[d,"F(f)"'] & G(A) \ar[d,"G(f)"] \\
      F(B) \ar[r,"\alpha_B"] & G(B)
    \end{tikzcd}
  \]
  in $\mathcal D$
  for each arrow $f : A \to_{\mathcal C} B$.\footnote{%
    These squares are called the ``naturality squares'' for $\alpha$.}

  If $\mathcal D$ is a precategory, then the types of the naturality square fillers
  are propositions. In this case, we just call $\alpha$ a \emph{natural transformation}.
\end{definition}
\begin{example}
  There is a wild
  natural transformation $\eta : \id_{\UU} \to ((\blank)_+)_\div$
  from the identity wild functor on the universe $\UU$
  to the composition
  \[
    \UU \xrightarrow{(\blank)_+} \UUp \xrightarrow{(\blank)_\div} \UU
  \]
  of the wild functors from~\cref{ex:add-remove-basepoint}.
  Its action on objects is $\inl{} : A \to (A_+)_\div$,
  where $(A_+)_\div \jdeq A \coprod\bn 1$.
  The naturality squares commute by reflexivity.
\end{example}
\begin{example}\label{ex:path-gpd-nat}
  Every function $f : A \to B$ between types in $\UU$
  becomes a wild functor between the corresponding wild path groupoids
  using the action on paths, $\ap f$ from~\cref{def:ap}.

  Likewise, given two functions $f,g : A \to B$, we get for
  every family of identifications $h : \prod_{x:A} f(x) \eqto g(x)$
  a wild natural transformation between the corresponding wild functors,
  using the naturality squares of~\cref{def:naturality-square}.
\end{example}

With natural transformations as arrows we can elevate the
type of functors to a precategory.
\begin{definition}
  For a wild precategory $\mathcal C$ and a precategory $\mathcal D$
  we have the \emph{functor precategory}\index{functor category}%
  \index{functor precategory|see{functor category}}
  $\mathcal C \to \mathcal D$, also written
  $[\mathcal C,\mathcal D]$ or $\mathcal D^{\mathcal C}$, % or $\constant{Fun}(\mathcal C,\mathcal D)$,%
  has functors from $\mathcal C$ to $\mathcal D$ as objects
  and natural transformations as arrows.
  The identity arrow at $F$ is the identity natural transformation
  $\id_F: F \to F$ that assigns to each object $A:\mathcal C$ the identity
  arrow $\id_{F(A)}$.
  The composition likewise forms compositions objectwise.
\end{definition}
\begin{xca}
  Show that a natural transformation $\alpha : F \to G$
  in a functor precategory $\mathcal C\to\mathcal D$
  is invertible if and only if
  each component $\alpha_A : F(A) \to_{\mathcal D} G(A)$ is.
\end{xca}
\begin{xca}
  Show that the functor precategory $\mathcal C\to\mathcal D$
  is univalent if $\mathcal D$ is.\footnote{%
    This is Thm.~9.2.5 in the HoTT book\footnotemark{}.}%
  \footcitetext{hottbook}
  In this case we call it the \emph{functor category}.
\end{xca}
\begin{xca}
  Let $A$ be a type and $\mathcal C$ category.
  Show that restricting to the action on objects
  induces an equivalence
  \[
    (A \to \mathcal C) \to (A \to \constant{Ob}(\mathcal C))
  \]
  from the functor category whose domain is the wild path category of $A$
  to the type of functions from $A$ to the objects of $\mathcal C$.
\end{xca}

A functor $F : \mathcal C\op \to \mathcal D$ whose domain is an opposite
category is called \emph{contravariant}, because it reverses the directions
of arrows: $f : C \to_{\mathcal C} C'$ in $\mathcal C$ maps to
$F(f) : F(C') \to_{\mathcal D} F(C)$ in $\mathcal D$.
If needed for emphasis, we may say that a functor
$F : \mathcal C \to \mathcal D$ is \emph{covariant} by contrast.

\begin{example}
  For an object $C$ of a \emph{locally $\UU$-small}
  wild precategory $\mathcal C$, we can form the
  co-
  and contravariant wild
  functors
  \begin{align*}
    \Hom_{\mathcal C}(C, \blank) &: \mathcal C \to \UU, \\
    \Hom_{\mathcal C}(\blank, C) &: \mathcal C\op \to \UU,
  \end{align*}
  whose actions on morphisms
  are by post- and precomposition, respectively.
  These are called \emph{representable} functors.
\end{example}

\section{Adjunctions}
\label{sec:adjunctions}

We have already seen two examples of an adjunctions
in~\cref{xca:adjunction-_!-^*,xca:adjunction-^*-_*}.
Given a group homomorphism $f : G \to H$,
there are families of bijections
\begin{align*}
  \alpha &: \Hom_H(f_!\,X,Y) \isoto \Hom_G(X,f^*\,Y), \\
  \beta &: \Hom_G(f^*\,Y,X) \isoto \Hom_H(Y,f_*\,X),
\end{align*}
for $G$-sets $X$ and $H$-sets $Y$
that are furthermore \emph{natural}.
This just means that if we fix either $X$ or $Y$,
then we get natural transformations of corresponding functors.
For example,
fixing $X$, we can regard $\alpha$ as a natural transformation
\[
  \alpha : \Hom_H(f_!\,X, \blank) \to \Hom_G(X, f^*\,\blank)
\]
from the representable functor for $\GSet[H]$ at $f_!\,X$
to the composition of $f^*$ and the representable functor
for $\GSet$ at $X$.

\begin{definition}\label{def:adjunction}
  A (\emph{wild}) \emph{adjunction} between two (wild) precategories
  $\mathcal C$ and $\mathcal D$ consists of:
  \begin{itemize}
  \item a (wild) functor $F : \mathcal C \to \mathcal D$ (the \emph{left adjoint}),
  \item a (wild) functor $G : \mathcal D \to \mathcal C$ (the \emph{right adjoint}),
  \item a (wild) natural isomorphism $\alpha : \Hom_{\mathcal D}(F\blank,\blank) \isoto
    \Hom_{\mathcal C}(\blank, G\blank)$.
  \end{itemize}
  We write $F \dashv G$ to denote this situation.%
  \glossary(2dashv){$\protect\dashv$}{adjunction}
\end{definition}
The essence of an adjunction is thus the ability to
transpose between arrows $F(C) \to_{\mathcal D} D$ and
$C \to_{\mathcal C} G(D)$.
There is however another way of packaging this information.
We can transpose the identity $\id_{F(C)}$
to get an arrow $\eta_C : C \to_{\mathcal C} GF(C)$,
and the identity $\id_{G(D)}$ to get an arrow
$\varepsilon_D : FG(D) \to_{\mathcal D} D$.
Naturality of $\alpha$ makes these into natural transformations
\[
  \eta : \id_{\mathcal C} \to GF,\quad\text{and}\quad
  \varepsilon : FG \to \id_{\mathcal D}
\]
called the \emph{unit} and \emph{counit} of the adjunction.
\begin{marginfigure}
  \[
    \begin{tikzcd}[ampersand replacement=\&,column sep=small]
      FGF(C) \ar[r,"\varepsilon_{F(C)}"] \& F(C) \\
      F(C) \ar[u,"F(\eta_C)"]\ar[ur,"\id_{F(C)}"'] \& \\[-5mm]
      \& G(D) \\
      G(D) \ar[ur,"\id_{G(D)}"]\ar[r,"\eta_{G(D)}"'] \& GFG(D) \ar[u,"G(\varepsilon_D)"']
    \end{tikzcd}
  \]
  \caption{Triangle laws for an adjunction $F \dashv G$.}
  \label{fig:adj-triangles}
\end{marginfigure}
\begin{xca}
  Use naturality of $\alpha$, along with unit laws to fill the
  triangle laws in~\cref{fig:adj-triangles}.
\end{xca}
Conversely, given $F$, $G$, $\eta$, and $\varepsilon$, along with
fillers for the triangle laws, we can recover $\alpha$
by sending $f : F(C) \to_{\mathcal D} D$ to
the composite
\[
  C \xrightarrow{\eta_C} GF(C) \xrightarrow{G(f)} G(D).
\]
\begin{xca}
  Use the functor and triangle laws to check that $\alpha$ thus
  defined is a natural isomorphism.
\end{xca}
%% How far are these from being an equivalence?


\begin{example}
  We have a wild adjunction $\Trunc\blank_n \dashv \iota_n$
  with $\Trunc\blank_n : \UU \to \UU^{\le n}$ (cf.~\cref{def:n-trunc-functor})
  as the left adjoint
  and the inclusion $\iota_n : \UU^{\le n} \to \UU$ as the right adjoint.
  Indeed, the constructor $\trunc\blank_n$ acts as the unit, precomposition with which
  gives the equivalence
  \[
    (\Trunc X_n \to Y) \equivto (X \to Y)
  \]
  for $X : \UU$ and $Y : \UU^{\le n}$.
\end{example}
\begin{example}
  Also the add/forget base points functors
  from~\cref{ex:add-remove-basepoint} can be arranged
  into a wild adjunction $(\blank)_+ \dashv (\blank)_\div$.
  For $A : \UUp$ and $X : \UU$ we have
  \[
    \alpha : (A_+ \ptdto X) \equivto (A \to X_\div)
  \]
  given by precomposition with $\inl{} : A \to A_+$.
\end{example}


% being a left adjoint is a proposition (after yoneda?)
% equivalences of categories
% fundamental theorem (fully faithful+eso = equivalence)
% cor: Cat is a 2-type
% rezk completion
% straightening–unstraightening
% precategories are flagged categories

\section{Limits and Colimits}
\label{sec:limits}

% products and coproducts, pullbacks and pushouts, (co)equalizers, (co)limits

\section{The Yoneda Lemma}
\label{sec:yoneda}

% product and exponential in types
% Yoneda lemma
% cor : \yo is fully faithful
% 

\section{Monoidal categories}
\label{sec:monoidal-cats}

% monoidal category = Mon(Cat)
% closed category (no need for HITs)

%% Move to Abstract Groups
% pregroupoids with Ob contr = abstract groups
% 

%%% Local Variables:
%%% mode: LaTeX
%%% latex-block-names: ("lemma" "theorem" "remark" "definition" "corollary" "fact" "properties" "conjecture" "proof" "question" "proposition" "exercise")
%%% TeX-master: "book"
%%% TeX-command-extra-options: "-fmt=macros"
%%% compile-command: "make book.pdf"
%%% End: