cats.tex

\documentclass[reqno]{amsart}

\usepackage{amssymb}
\usepackage{hyperref}
\usepackage{mathtools}
\usepackage[all]{xy}
\usepackage{verbatim}
\usepackage{ifthen}
\usepackage{xargs}
\usepackage{bussproofs}
\usepackage{turnstile}
\usepackage{etex}

\hypersetup{colorlinks=true,linkcolor=blue}

\newcommand{\axlabel}[1]{(#1) \phantomsection \label{ax:#1}}
\newcommand{\axtag}[1]{\label{ax:#1} \tag{#1}}
\newcommand{\axref}[1]{(\hyperref[ax:#1]{#1})}

\newcommand{\newref}[4][]{
\ifthenelse{\equal{#1}{}}{\newtheorem{h#2}[hthm]{#4}}{\newtheorem{h#2}{#4}[#1]}
\expandafter\newcommand\csname r#2\endcsname[1]{#3~\ref{#2:##1}}
\expandafter\newcommand\csname R#2\endcsname[1]{#4~\ref{#2:##1}}
\expandafter\newcommand\csname n#2\endcsname[1]{\ref{#2:##1}}
\newenvironmentx{#2}[2][1=,2=]{
\ifthenelse{\equal{##2}{}}{\begin{h#2}}{\begin{h#2}[##2]}
\ifthenelse{\equal{##1}{}}{}{\label{#2:##1}}
}{\end{h#2}}
}

\newref[section]{thm}{Theorem}{Theorem}
\newref{lem}{Lemma}{Lemma}
\newref{prop}{Proposition}{Proposition}
\newref{cor}{Corollary}{Corollary}
\newref{cond}{Condition}{Condition}

\theoremstyle{definition}
\newref{defn}{Definition}{Definition}
\newref{example}{Example}{Example}

\theoremstyle{remark}
\newref{remark}{Remark}{Remark}

\newcommand{\fs}[1]{\mathrm{#1}}
\newcommand{\cat}[1]{\mathbf{#1}}
\newcommand{\scat}[1]{\mathcal{#1}}
\newcommand{\Hom}{\fs{Hom}}
\renewcommand{\hom}{\fs{hom}}
\newcommand{\id}{\fs{id}}
\newcommand{\Id}{\fs{Id}}
\newcommand{\Set}{\cat{Set}}
\newcommand{\uSet}{\fs{Set}}
\newcommand{\uType}{\fs{Type}}
\newcommand{\ob}[1]{#1_0}
\newcommand{\fob}[1]{#1_0}
\newcommand{\Prop}{\fs{Prop}}
\newcommand{\El}{\fs{El}}

\numberwithin{figure}{section}

\newcommand{\pb}[1][dr]{\save*!/#1-1.2pc/#1:(-1,1)@^{|-}\restore}
\newcommand{\po}[1][dr]{\save*!/#1+1.2pc/#1:(1,-1)@^{|-}\restore}

\begin{document}

\title{Cats}

\author{Valery Isaev}

\begin{abstract}
% TODO
\end{abstract}

\maketitle

\section{Introduction}

% TODO

\section{Basic category theory}

In this section, we recall the definition of categories and basic constructions on them in homotopy type theory.
We also give definitions of a few constructions.
All of them are standard categorical constructions and their definitions can be found, for example, in \cite{maclane}.
We will only state most of the theorems since their proofs are identical to the standard ones.

\subsection{Definitions}

The purpose of this subsection is mostly to recall definitions from \cite{univalent-cats} and to fix the notation.

A \emph{precategory} $\scat{C}$ consists of a type of objects $\ob{\scat{C}}$ (which we often denote simply by $\scat{C}$), a set of maps $\hom_\scat{C}(x,y)$ for every pair of objects $x,y : \scat{C}$,
an associative composition function $\circ : \hom_\scat{C}(y,z) \to \hom_\scat{C}(x,y) \to \hom_\scat{C}(x,z)$, and an identity morphism $\id_x : \hom_\scat{C}(x,x)$ which is a two-sided identity for $\circ$.
We will omit the subscript in $\hom_\scat{C}(x,y)$ if the category is clear from the context.
A precategory is a \emph{category} if the obvious map from $\Id(x,y)$ to the type of isomorphisms between any pair of objects $x$ and $y$ is an equivalence.

A \emph{functor} between precategories $\scat{C}$ and $\scat{D}$ consists of a map $\fob{F} : \ob{\scat{C}} \to \ob{\scat{D}}$ (which we often denote simply by $F$)
together with a map $F : \hom_\scat{C}(x,y) \to \hom_\scat{D}(F(x),F(y))$ for every pair of objects $x$ and $y$ such that $F$ preserves identity morphisms and composition.
A natural transformation between functors $F,G : \scat{C} \to \scat{D}$ is a map $\alpha_x : \hom_\scat{D}(F(x),G(x))$ defined for every object $x : \scat{C}$ such that $G(f) \circ \alpha_x = \alpha_y \circ F(f)$ for every map $f : \hom_\scat{C}(x,y)$.
Functors and natural transformations form a precategory $\scat{D}^\scat{C}$ which is a category whenever $\scat{D}$ is.

A functor $F : \scat{C} \to \scat{D}$ is \emph{faithful} (resp., \emph{full}, \emph{fully faithfull}) if the map $F : \hom_\scat{C}(x,y) \to \hom_\scat{D}(F(x),F(y))$ is injective (resp., surjective, bijective) for all $x$ and $y$.
We will call fully faithfull functors \emph{embeddings}.
A functor $F : \scat{C} \to \scat{D}$ is essentially surjective on objects if, for every $y : \scat{D}$, there merely exists an object $x : \scat{C}$ such that $F(x)$ is isomorphic to $y$.
For every precategory $\scat{C}$, there exists a category $\widehat{\scat{C}}$ together with an essentially surjective embedding $i_\scat{C} : \scat{C} \to \widehat{\scat{C}}$.
The category $\widehat{\scat{C}}$ is called \emph{the Rezk completion of $\scat{C}$}.
It satisfies a universal property: for every category $\scat{D}$ and every functor $F : \scat{C} \to \scat{D}$, there is a unique functor $\widehat{F} : \widehat{\scat{C}} \to \scat{D}$ such that $\widehat{F} \circ i_\scat{C} = F$.

Let $\uType$ be a universe closed under unit types, identity types, $\Sigma$-types, $\Pi$-types, empty types, pushouts, set trunctions, and 1-truncations.
Let $\uSet$ be its subuniverse of sets.
Then we have the category $\Set$ whose types are elements of $\uSet$ and maps are functions.
A precategory $\scat{C}$ is \emph{locally small} (with respect to $\uSet$) if the set of maps $\hom_\scat{C}(x,y)$ is equivalent to a set in $\uSet$ for all $x$ and $y$.
A precategory $\scat{C}$ is \emph{small} (with respect to $\uType$) if it is locally small and the type of objects of $\scat{C}$ is equivalent to a type in $\uType$.

\begin{example}
The category $\Set$ is locally small since $\uSet$ is closed under function types.
\end{example}

\begin{example}
The Rezk completion of a small precategory is a small category.
\end{example}

The \emph{opposite} of a (pre)category $\scat{C}$ is the (pre)category $\scat{C}^\fs{op}$ with the same type of objects in which the set of maps is defined as follows: $\hom_{\scat{C}^\fs{op}}(x,y) = \hom_\scat{C}(y,x)$.
For every locally small precategory $\scat{C}$, there is an embedding $\cat{y} : \scat{C} \to \Set^{\scat{C}^\fs{op}}$ called \emph{Yoneda embedding}.
It is defined by the formula $\cat{y}(x) = \hom_\scat{C}(-,x)$.

\subsection{Full subcategories}

A \emph{full subprecategory} of a precategory $\scat{D}$ is a type over $\ob{\scat{D}}$.
A \emph{full subcategory} of a category $\scat{D}$ is a proposition over $\ob{\scat{D}}$.
A \emph{(pre)category embedded in $\scat{D}$} is a (pre)category $\scat{C}$ together with an embedding $\scat{C} \to \scat{D}$.
The following lemma shows that these notions are equivalent:

\begin{lem}
Full subprecategories of a precategory $\scat{D}$ are equivalent to precategories embedded in $\scat{D}$.
Full subcategories of a category of $\scat{D}$ are equivalent to categories $\scat{C}$ embedded in $\scat{D}$.
\end{lem}
\begin{proof}
Let $P$ be a type over $\ob{\scat{D}}$.
We define a precategory $\scat{C}_P$ and an embedding $F_P : \scat{C}_P \to \scat{D}$.
The type of objects of $\scat{C}_P$ is defined as $\Sigma_{x : \ob{\scat{D}}} P(x)$.
The set of maps $\hom_{\scat{C}_P}((x,p),(x',p'))$ is defined as $\hom_\scat{D}(x,x')$.
The composition and identity maps are defined in the same way as in $\scat{D}$.
The functor $F_P : \scat{C}_P \to \scat{D}$ is defined in the obvious way: $F_P(x,p) = x$ for an object $(x,p)$ and $F_P(f) = f$ for a map $f$.
Clearly, $F_P$ is an embedding.
Now, let $\scat{C}$ be a precategory and let $F : \scat{C} \to \scat{D}$ be an embedding.
We define a type $P_F(x)$ for every $x : \ob{\scat{D}}$ as follows: $P_F(x) = \Sigma_{y : \ob{\scat{C}}} \Id(F(y),x)$.

Let us prove that constructions that we described are mutually inverse.
Let $P$ be a type over $\ob{\scat{D}}$.
Then $P_{F_P}(x)$ is equivalent to $\Sigma_{x' : \ob{\scat{D}}} P(x') \times \Id(x',x)$ which is equivalent to $P(x)$.
Let $F : \scat{C} \to \scat{D}$ be an embedding.
We need to prove that $\scat{C}$ is isomorphic to $\scat{C}_{P_F}$.
The type of objects of the latter precategory is defined as $\Sigma_{x : \ob{\scat{D}}} \Sigma_{y : \ob{\scat{C}}} \Id(F(y),x)$ which is equivalent to $\ob{\scat{C}}$.
Thus, we have an obvious isomorphism $G : \scat{C} \to \scat{C}_{P_F}$.
The equality $F_{P_F} \circ G = F$ holds by definition.
This completes the proof of the first assertion.

Now, let us prove the second assertion.
Let $\scat{D}$ be a category.
Let $P$ be a type over $\ob{\scat{D}}$ such that, for every $x : \ob{\scat{D}}$, the type $P(x)$ is a proposition.
We need to show that $\scat{C}_P$ is a category.
Indeed, since $P(x)$ is a proposition, the type $\Id((x,p),(x',p'))$ of paths between objects $(x,p)$ and $(x',p')$ of $\scat{C}_P$ is equivalent to $\Id(x,x')$,
which is equivalent to the type $x \simeq y$ of isomorphisms of $x$ and $x'$ since $\scat{D}$ is a category and $x \simeq y$ is equivalent to $(x,p) \simeq (x',p')$ by the definition of $\scat{C}_P$.
Now, let $\scat{C}$ be a category and let $F : \scat{C} \to \scat{D}$ be an embedding.
We need to show that $P_F(x)$ is a proposition for every $x : \ob{\scat{D}}$.
Since $\scat{C}$ and $\scat{D}$ are categories and $F$ is an embedding of categories, it follows that $\fob{F}$ is an embedding of types.
Since $P_F(x)$ is a fiber of $\fob{F}$ over $x$ and $\fob{F}$ is an embedding, it follows that $P_F(x)$ is a proposition.
This completes the proof.
\end{proof}

A full subprecategory $P$ is \emph{small} with respect to a universe $\uType$ if $P(x)$ is equivalent to a type in $\uType$ for every $x : \ob{\scat{D}}$.
Thus, a full subprecategory of $\scat{D}$ is simply a map $\ob{\scat{D}} \to \uType$.
If $\scat{D}$ is small, then the equivalences defined in the previous lemma restrict to equivalences between small full sub(pre)categories of $\scat{D}$ and small (pre)categories embedded in $\scat{D}$.

% In general, we do not have a type of full subprecategories of a given precategory, but we do have a type of full subcategories of a given category if we have a subtype classifier
% (that is, a univalent universe $\Prop$ consisting of propositions such that, for every proposition $P$, there exists an element $\chi_P : \Prop$ such that $\El(\chi_P)$ is equivalent to $P$).

Adjoint functors are defined as usual.
If $\scat{C}$ is a category and $F : \scat{C} \to \scat{D}$ is a functor, then there is a unique left (or right) adjoint to $F$ if it exists.
We will say that a subprecategory $P$ of a precategory $\scat{D}$ is \emph{reflective} if the corresponding embedding $F_P : \scat{C}_P \to \scat{D}$ has a left adjoint.
If $\scat{D}$ is a category and $P$ is a subcategory, then this is a property of $P$, but in general this is an additional structure on $P$.
Equivalently, a reflective subprecategory of $\scat{D}$ can be described as a reflector $R : \ob{\scat{D}} \to \ob{\scat{D}}$
together with a proof $P(R(x))$ and a map $\eta_x : \hom(x,R(x))$ for every $x : \ob{\scat{D}}$ satisfying the following universal property.
For every $y : \scat{D}_0$ such that $P(y)$ and every map $f : \hom(x,y)$, there is a unique map $\widehat{f} : \hom(R(x),y)$ such that $\widehat{f} \circ \eta_x = f$.

\subsection{Kan extensions}

Kan extensions are defined as usual.
Let $p : \scat{J} \to \scat{J}'$ be a functor between precategories.
A \emph{left Kan extension} of a functor $F : \scat{J} \to \scat{D}$ along $p$ is a functor $\fs{Lan}_p(F) : \scat{J}' \to \scat{D}$
together with a natural transformation $\alpha : \hom_{\scat{D}^\scat{J}}(F, \fs{Lan}_p(F) \circ p)$ such that the following function is a bijection:
\begin{align*}
\varphi_G & : \hom_{\scat{D}^{\scat{J}'}}(\fs{Lan}_p(F),G) \simeq \hom_{\scat{D}^\scat{J}}(F, G \circ p) \\
\varphi_G(\beta)_j & = \beta_{p(j)} \circ \alpha_j
\end{align*}
\emph{Right Kan extensions} are defined dually.

A \emph{limit} (resp., \emph{colimit}) of a functor $F : \scat{J} \to \scat{D}$ is a right (resp., left) Kan extension of $F$ along the unique functor $\scat{J} \to 1$.
A \emph{cone} (resp., \emph{cocone}) over $F$ is an object $d : \scat{D}$ together with a natural transformation $\alpha : \Delta(d) \to F$ (resp., $\alpha : F \to \Delta(d)$), where $\Delta(d)$ is the constant functor on $d$.
Thus, limits and colimits are cones and cocones satisfying a universal property.
It is easy to prove that left adjoints preserve colimits and right adjoints preserve limits.

\begin{example}
The category $\Set$ has small products since $\uType$ is closed under $\Pi$-types.
It has equalizers since $\uSet$ is closed under identity types and $\Sigma$-types.
It has small coproducts and coequalizers since $\uType$ is closed under empty types, pushouts, and set truncations.
\end{example}

We will say that a precategory is \emph{(co)complete} if it has (co)limits indexed by small precategories.
If $\scat{C}$ is a category that has (co)limits indexed by small categories, then $\scat{C}$ is (co)complete.
Indeed, every functor $F : \scat{J} \to \scat{C}$ factors through the Rezk completion of $\scat{J}$ and the (co)limit of the corresponding functor $\widehat{\scat{J}} \to \scat{C}$ coincides with the colimit of $F$.

We can also define (co)limits of diagrams indexed by types in the obivous way.
We call such (co)limits \emph{(co)products}.
For every type $\scat{J}$, we can define a precategory $\scat{J}'$ that has $\scat{J}$ as the type of objects and $\| \Id(j,j') \|_0$ as the set of maps from $j$ to $j'$.
Since $\uType$ is closed under identity types, $\scat{J}'$ is small whenever $\scat{J}$ is.
Every diagram $F : \scat{J} \to \scat{C}$ factors through $\scat{J}'$.
The (co)product of $F$ coincides with the (co)limit of the corresponding functor $\scat{J}' \to \scat{C}$.

As usual, (co)limits indexed by a precategory $\scat{J}$ can be defined in terms of (co)equalizers and (co)products indexed by $\ob{\scat{J}}$ and $\hom(\scat{J}) = \Sigma_{x y : \ob{\scat{J}}} \hom(x,y)$.
In general, $\ob{\scat{J}}$ and $\hom(\scat{J})$ are arbitrary types.
Note that (co)products indexed by a type are more general than (co)products indexed by a set.
For example, a (co)product of a diagram $F : S^1 \to \scat{C}$ is a (co)equalizer of $\id_{F(*)} : \hom(F(*),F(*))$ and the map corresponding to $F(\fs{loop}) : \Id(F(*),F(*))$.

Let $F : \scat{J}^\fs{op} \times \scat{J} \to \scat{C}$ be a functor.
A \emph{dinatural transformation} is a collection of maps $\alpha_j : \hom(F(j,j),c_0)$ defined for all $j : \scat{J}$ such that the following square commutes for every map $f : \hom(j,j')$:
\[ \xymatrix{ F(j',j) \ar[r]^{F(f,\id_j)} \ar[d]_{F(\id_{j'},f)}    & F(j,j) \ar[d]^{\alpha_j} \\
              F(j',j') \ar[r]_-{\alpha_{j'}}                        & c_0
            } \]
A \emph{coend} of a functor $F : \scat{J}^\fs{op} \times \scat{J} \to \scat{C}$ is an object $c_0$ together with a dinatural transformation $\alpha$ such that,
for every $c : \scat{C}$ and every dinatural transformation $\beta_j : \hom(F(j,j),c)$, there is a unique map $f : \hom(c_0,c)$ such that $f \circ \alpha_j = \beta_j$.
\emph{Ends} are defined dually.
As usual, (co)ends can be described in terms of (co)limits.
An end (resp. coend) of a functor $F : \scat{J}^\fs{op} \times \scat{J} \to \scat{C}$ will be denoted by $\int_{j : \scat{J}} F(j,j)$ (resp., $\int^{j : \scat{J}} F(j,j)$).

\begin{remark}
Kan extensions, (co)limits, and (co)ends in a precategory $\scat{D}$ are unique only when $\scat{D}$ is a category.
\end{remark}

A left Kan extension of $F : \scat{J} \to \scat{D}$ along $p : \scat{J} \to \scat{J}'$ can be defined as a coend if it exists: $\fs{Lan}_p(F)(j') = \int^{j : \scat{J}} \hom(p(j),j') \cdot F(j)$.
In particular, if $F = \cat{y} : \scat{J} \to \Set^{\scat{J}^\fs{op}}$ is the Yoneda embedding, then $\fs{Lan}_p(\cat{y})(X) = \int^{j : \scat{J}} X(j) \cdot F(j)$.

\subsection{Final functors}

Let $F_1 : \scat{J}_1 \to \scat{C}$ and $F_2 : \scat{J}_2 \to \scat{C}$ be functors between precategories.
Then the \emph{comma precategory} $F_1 \downarrow F_2$ is defined as usual.
Its objects are triples $\Sigma_{j_1 : \scat{J}_1} \Sigma_{j_2 : \scat{J}_2} \hom(F_1(j_1),F_2(j_2))$.
Maps between $(j_1,j_2,f)$ and $(j_1',j_2',f')$ are pairs of maps $g_1 : \hom(j_1,j_1')$ and $g_2 : \hom(j_2,j_2')$ such that the obvious square commutes.
If $\scat{J}_1$ and $\scat{J}_2$ are categories, then $F_1 \downarrow F_2$ is also a category.
If $c$ is an object of $\scat{C}$ and $F : \scat{J} \to \scat{C}$ is a functor, then we will write $c \downarrow F$ for the comma category of the functor $1 \to \scat{C}$ that picks $c$ and $F$.

We will say that a precategory is \emph{inhabited} if it merely has an object.
We will say that a precategory $\scat{C}$ is \emph{connected} if, for every pair of objects $c$ and $c'$, there merely exists a sequence of objects $c_1$, \ldots $c_n$ and a sequence of maps $f_1$, \ldots $f_{n-1}$
such that $c_1 = c$, $c_n = c'$, and, for every $1 \leq i < n$, either $\fs{dom}(f_i) = c_i$ and $\fs{cod}(f_i) = c_{i+1}$ or $\fs{dom}(f_i) = c_{i+1}$ and $\fs{cod}(f_i) = c_i$.
A functor $L : \scat{I} \to \scat{J}$ is \emph{final} if, for every $j : \scat{J}$, the comma category $j \downarrow L$ is inhabited and connected.

\begin{lem}
Let $L : \scat{I} \to \scat{J}$ be a final functor and let $F : \scat{J} \to \scat{C}$ be a functor.
Then $\fs{colim}(F)$ exists if and only if $\fs{colim}(F \circ L)$ exists and the canonical map $\hom_\scat{C}(\fs{colim}(F \circ L),\fs{colim}(F))$ is an isomorphism.
\end{lem}
\begin{proof}
% TODO
\end{proof}

\begin{prop}
Let $L : \scat{I} \to \scat{J}$ be a functor between locally small categories.
Then the following conditions are equivalent:
\begin{enumerate}
\item $L$ is final.
\item For every functor $F : \scat{J} \to \scat{C}$, a colimit $\fs{colim}(F)$ exists if and only if $\fs{colim}(F \circ L)$ exists and the canonical map $\hom_\scat{C}(\fs{colim}(F \circ L),\fs{colim}(F))$ is an isomorphism.
\item For every functor $F : \scat{J} \to \Set$, the canonical map $\fs{colim}(F \circ L) \to \fs{colim}(F)$ is an isomorphism.
\item For every $j : \scat{J}$, the set $\fs{colim}_{i : I} \hom_\scat{J}(j,L(i))$ is contractible.
\end{enumerate}
\end{prop}
\begin{proof}
% TODO
\end{proof}

% TODO: Directed and filtered colimits.

\subsection{Dense subcategories and generators}

Let $F : \scat{C} \to \scat{D}$ be a functor between precategories, let $d$ be an object of $\scat{D}$, and let $D_F$ be the diagram $F \downarrow d \to \scat{C} \xrightarrow{F} \scat{D}$.
Then we have a canonical cocone $\alpha^d : D_F \to \Delta(d)$ defined by $\alpha^d_{(X,f)} = f$.
A functor $F : \scat{C} \to \scat{D}$ is \emph{dense} if, for every $d : \scat{D}$, the cocone $\alpha^d$ is the colimit of $D_F$.
The following proposition follows from the usual easy formal argument:

\begin{prop}
Let $\scat{D}$ be a locally small precategory.
Then a functor $F : \scat{C} \to \scat{D}$ is dense if and only if the nerve functor $N_F : \scat{D} \to \Set^{\scat{C}^\fs{op}}$, defined by $N_F(d) = \hom_\scat{D}(F(-),d)$, is fully faithful.
\end{prop}
% \begin{proof}
% A natural transformation between $N_F(d)$ and $N_F(d')$ is a function $\alpha_c : \hom_\scat{D}(F(c),d) \to \hom_\scat{D}(F(c),d')$ such that,
% for all $f : \hom_\scat{C}(c,c')$ and $g : \hom_\scat{D}(F(c'),d)$, it is true that $\alpha_{c'}(g) \circ F(f) = \alpha_c(g \circ F(f))$.
% Thus, there is a bijection between such natural tranformations and cocones of the form $D_F \to \Delta(d')$.
% Then $d$ is a colimit if and only if, for every $d' : \scat{D}$, the map from $\hom_\scat{D}(d,d')$ to the set of cocones is a bijections,
% which is true if and only if the map from $\hom_\scat{D}(d,d')$ to the set of natural transformations between $N_F(d)$ and $N_F(d')$ is a bijection.
% \end{proof}

We will say that a full subprecategory is dense if the corresponding embedding is dense.
A weaker notion than that of a dense subprecategory is the notion of an (extremal) generator.
A \emph{generator} of a precategory $\scat{C}$ is a subprecategory $\scat{G}$ such that two maps $f,g : \hom_\scat{C}(X,Y)$ are equal whenever $f \circ x = g \circ x$ for all $G : \scat{G}$ and $x : \hom_\scat{C}(G,X)$.
An \emph{extremal generator} of a precategory $\scat{C}$ is a subprecategory $\scat{G}$ such that a monomorphism $m : \hom_\scat{C}(X,Y)$ is an isomorphism whenever every map $\hom_\scat{C}(Z,Y)$ such that $Z$ belongs to $\scat{G}$ factors through $m$.

Finally, let us define yet another useful notion.
We will say that a subprecategory $\scat{D}$ of a precategory $\scat{C}$ is \emph{colimit-dense} if every object of $\scat{C}$ is merely a colimit of objects from $\scat{D}$.
Every dense subprecategory is colimit-dense and every colimit-dense subprecategory is a generator and an extremal generator.
If a precategory has equalizers, then every extremal generator is a generator.

\subsection{Adjoint functor theorems}

First, we need to state the initial object theorem:

\begin{lem}[initial]
Let $\scat{C}$ be a locally small complete precategory.
Then it has an initial object if and only if there is a small family of objects $\{ w_i \}_{i : I}$ of $\scat{C}$ such that, for every $c : \scat{C}$, there merely exists $i : I$ and a map from $w_i$ to $c$.
If $\scat{C}$ is a category, then it is enough to assume that there merely exists such a family.
\end{lem}
\begin{proof}
See, for example, \cite[Theorem~V.6.1]{maclane}.
The proof there applies verbatim.
\end{proof}

Now, we can prove the general adjoint functor theorem:

\begin{thm}[gaft]
Let $\scat{D}$ be a locally small complete precategory and let $\scat{C}$ be a precategory.
Suppose that either $\uSet$ contains all propositions or $\scat{C}$ is locally small.
The a functor $G : \scat{D} \to \scat{C}$ has a left adjoint if and only if it preserves limits and, for every $c : \scat{C}$, there is a small family of maps $\{ f_i : \hom_\scat{C}(c,G(d_i)) \}_{i : I}$
such that, for every map $h : \hom_\scat{C}(c,G(d))$, there merely exists $i : I$ and a map $t : \hom_\scat{D}(d_i,d)$ such that $h = G(t) \circ f_i$.
If $\scat{D}$ is a category, then it is enough to assume that there merely exists such a family for every $c : \scat{C}$.
\end{thm}
\begin{proof}
The ``only if'' direction is obvious.
To prove the converse, we can apply \rlem{initial} to the precategory $c \downarrow G$ since a left adjoint to $G$ exists if and only if this precategory has an initial object for every $c : \scat{C}$.
The assumptions on $\scat{D}$ imply that $c \downarrow G$ is locally small and complete as proved in \cite[Theorem~V.6.2]{maclane}.
\end{proof}

A precategory is \emph{well-powered} if the type of subobjects (that is, equivalences classes of monomorphisms) of every object is small.
The special adjoint functor theorem can be proved as usual:

\begin{thm}[saft]
Let $G : \scat{D} \to \scat{C}$ be a functor between locally small precategories.
Suppose that $\scat{D}$ is well-powered, complete, and has a small cogenerating set.
Then $G$ has a left adjoint if and only if it preserves limits.
\end{thm}
\begin{proof}
The proof is the same as in \cite[Theorem~V.8.2]{maclane}.
\end{proof}

Finally, let us prove yet another version of the adjoint functor theorem:

\begin{thm}[yaraft]
Let $G : \scat{D} \to \scat{C}$ be a functor between locally small precategories.
Suppose that $\scat{D}$ is complete and has a small full subprecategry $\scat{D}'$ such that every object of $\scat{D}$ is merely a limit of objects in $\scat{D}'$.
Then $G$ has a left adjoint if and only if it preserves limits.
\end{thm}
\begin{proof}
By \rthm{gaft}, it is enough to show that, for every $c : \scat{C}$, there is a map $f : \hom(c,G(d_0))$ such that every map $h : \hom(c,G(d))$ merely factors through $f$.
Let $I$ be the embedding $c \downarrow G|_{\scat{D}'} \to c \downarrow G$.
Since $\scat{D}'$ is small and $\scat{C}$ is locally small, the precategory $c \downarrow G|_{\scat{D}'}$ is small.
Let $f : \hom(c,G(d_0))$ be the limit of $I$ (the fact that $c \downarrow G$ is complete is proved in \cite[Theorem~V.6.2]{maclane}).
Let $h : \hom(c,G(d))$ be a map.
By assumption, $d \simeq \fs{lim}_{j : \scat{J}} d_j$, where objects $d_j$ belong to $\scat{D}'$.
Since $G$ preserves limits, we may assume that $h$ is of the form $\hom(c,\fs{lim}_{j : \scat{J}} G(d_j))$.
Since $f$ is a limit of objects of the form $\hom(c,G(d'))$, we have a cone $\alpha_j : \hom(G(d_0),G(d_j))$ under $c$.
It follows that there is a map $\hom(G(d_0), \fs{lim}_{j : \scat{J}} d_j)$ under $c$.
Thus, $h$ factors through $f$.
\end{proof}

The previous theorem is useful in its dual form:

\begin{cor}[yalaft]
Let $F : \scat{C} \to \scat{D}$ be a functor between locally small precategories.
Suppose that $\scat{C}$ is cocomplete and has a small colimit-dense subprecategory.
Then $F$ has a right adjoint if and only if it preserves colimits.
\end{cor}

\bibliographystyle{amsplain}
\bibliography{ref}

\end{document}