9.6 Strict categories
Definition 9.6.1.
A strict category is a precategory whose type of objects is a set.
In accordance with the mathematical red herring principle, a strict category is not necessarily a category^{}. In fact, a category is a strict category precisely when it is gaunt (\autorefct:gaunt). Most of the time, category theory^{} is about categories, not strict ones, but sometimes one wants to consider strict categories. The main advantage of this is that strict categories have a stricter notion of “sameness” than equivalence, namely isomorphism^{} (or equivalently, by \autorefct:cateqiso, equality).
Here is one origin of strict categories.
Example 9.6.2.
Let $A$ be a precategory and $x\mathrm{:}A$ an object. Then there is a precategory $\mathrm{mono}\mathit{}\mathrm{(}A\mathrm{,}x\mathrm{)}$ as follows:

•
Its objects consist of an object $y:A$ and a monomorphism^{} $m:{\mathrm{hom}}_{A}(y,x)$. (As usual, $m:{\mathrm{hom}}_{A}(y,x)$ is a monomorphism (or is monic) if $(m\circ f=m\circ g)\Rightarrow (f=g)$.)

•
Its morphisms from $(y,m)$ to $(z,n)$ are arbitrary morphisms from $y$ to $z$ in $A$ (not necessarily respecting $m$ and $n$).
An equality $\mathrm{(}y\mathrm{,}m\mathrm{)}\mathrm{=}\mathrm{(}z\mathrm{,}n\mathrm{)}$ of objects in $\mathrm{mono}\mathit{}\mathrm{(}A\mathrm{,}x\mathrm{)}$ consists of an equality $p\mathrm{:}y\mathrm{=}z$ and an equality ${p}_{\mathrm{*}}\mathrm{\left(}m\mathrm{\right)}\mathrm{=}n$, which by \autorefct:idtoisotrans is equivalently an equality $m\mathrm{=}n\mathrm{\circ}\mathrm{idtoiso}\mathit{}\mathrm{(}p\mathrm{)}$. Since homsets are sets, the type of such equalities is a mere proposition. But since $m$ and $n$ are monomorphisms, the type of morphisms $f$ such that $m\mathrm{=}n\mathrm{\circ}f$ is also a mere proposition. Thus, if $A$ is a category, then $\mathrm{(}y\mathrm{,}m\mathrm{)}\mathrm{=}\mathrm{(}z\mathrm{,}n\mathrm{)}$ is a mere proposition, and hence $\mathrm{mono}\mathit{}\mathrm{(}A\mathrm{,}x\mathrm{)}$ is a strict category.
This example can be dualized, and generalized in various ways. Here is an interesting application of strict categories.
Example 9.6.3.
Let $E\mathrm{/}F$ be a finite Galois extension^{} of fields, and $G$ its Galois group. Then there is a strict category whose objects are intermediate fields $F\mathrm{\subseteq}K\mathrm{\subseteq}E$, and whose morphisms are field homomorphisms which fix $F$ pointwise (but need not commute with the inclusions into $E$). There is another strict category whose objects are subgroups $H\mathrm{\subseteq}G$, and whose morphisms are morphisms of $G$sets $G\mathrm{/}H\mathrm{\to}G\mathrm{/}K$. The fundamental theorem of Galois theory^{} says that these two precategories are isomorphic (not merely equivalent^{}).
Title  9.6 Strict categories 

\metatable 