## 4.39 Categories fibred in setoids

Definition 4.39.1. Let us call a category a setoid1 if it is a groupoid where every object has exactly one automorphism: the identity.

If $C$ is a set with an equivalence relation $\sim$, then we can make a setoid $\mathcal{C}$ as follows: $\mathop{\mathrm{Ob}}\nolimits (\mathcal{C}) = C$ and $\mathop{\mathrm{Mor}}\nolimits _\mathcal {C}(x, y) = \emptyset$ unless $x \sim y$ in which case we set $\mathop{\mathrm{Mor}}\nolimits _\mathcal {C}(x, y) = \{ 1\}$. Transitivity of $\sim$ means that we can compose morphisms. Conversely any setoid category defines an equivalence relation on its objects (isomorphism) such that you recover the category (up to unique isomorphism – not equivalence) from the procedure just described.

Discrete categories are setoids. For any setoid $\mathcal{C}$ there is a canonical procedure to make a discrete category equivalent to it, namely one replaces $\mathop{\mathrm{Ob}}\nolimits (\mathcal{C})$ by the set of isomorphism classes (and adds identity morphisms). In terms of sets endowed with an equivalence relation this corresponds to taking the quotient by the equivalence relation.

Definition 4.39.2. Let $\mathcal{C}$ be a category. A category fibred in setoids is a category fibred in groupoids all of whose fibre categories are setoids.

Below we will clarify the relationship between categories fibred in setoids and categories fibred in sets.

Definition 4.39.3. Let $\mathcal{C}$ be a category. The $2$-category of categories fibred in setoids over $\mathcal{C}$ is the sub $2$-category of the category of categories fibred in groupoids over $\mathcal{C}$ (see Definition 4.35.6) defined as follows:

1. Its objects will be categories $p : \mathcal{S} \to \mathcal{C}$ fibred in setoids.

2. Its $1$-morphisms $(\mathcal{S}, p) \to (\mathcal{S}', p')$ will be functors $G : \mathcal{S} \to \mathcal{S}'$ such that $p' \circ G = p$ (since every morphism is strongly cartesian $G$ automatically preserves them).

3. Its $2$-morphisms $t : G \to H$ for $G, H : (\mathcal{S}, p) \to (\mathcal{S}', p')$ will be morphisms of functors such that $p'(t_ x) = \text{id}_{p(x)}$ for all $x \in \mathop{\mathrm{Ob}}\nolimits (\mathcal{S})$.

Note that every $2$-morphism is automatically an isomorphism. Hence this $2$-category is actually a $(2, 1)$-category.

Here is the obligatory lemma on the existence of $2$-fibre products.

Lemma 4.39.4. Let $\mathcal{C}$ be a category. The 2-category of categories fibred in setoids over $\mathcal{C}$ has 2-fibre products. More precisely, the 2-fibre product described in Lemma 4.32.3 returns a category fibred in setoids if one starts out with such.

Proof. Omitted. $\square$

Lemma 4.39.5. Let $\mathcal{C}$ be a category. Let $\mathcal{S}$ be a category over $\mathcal{C}$.

1. If $\mathcal{S} \to \mathcal{S}'$ is an equivalence over $\mathcal{C}$ with $\mathcal{S}'$ fibred in sets over $\mathcal{C}$, then

1. $\mathcal{S}$ is fibred in setoids over $\mathcal{C}$, and

2. for each $U \in \mathop{\mathrm{Ob}}\nolimits (\mathcal{C})$ the map $\mathop{\mathrm{Ob}}\nolimits (\mathcal{S}_ U) \to \mathop{\mathrm{Ob}}\nolimits (\mathcal{S}'_ U)$ identifies the target as the set of isomorphism classes of the source.

2. If $p : \mathcal{S} \to \mathcal{C}$ is a category fibred in setoids, then there exists a category fibred in sets $p' : \mathcal{S}' \to \mathcal{C}$ and an equivalence $\text{can} : \mathcal{S} \to \mathcal{S}'$ over $\mathcal{C}$.

Proof. Let us prove (2). An object of the category $\mathcal{S}'$ will be a pair $(U, \xi )$, where $U \in \mathop{\mathrm{Ob}}\nolimits (\mathcal{C})$ and $\xi$ is an isomorphism class of objects of $\mathcal{S}_ U$. A morphism $(U, \xi ) \to (V , \psi )$ is given by a morphism $x \to y$, where $x \in \xi$ and $y \in \psi$. Here we identify two morphisms $x \to y$ and $x' \to y'$ if they induce the same morphism $U \to V$, and if for some choices of isomorphisms $x \to x'$ in $\mathcal{S}_ U$ and $y \to y'$ in $\mathcal{S}_ V$ the compositions $x \to x' \to y'$ and $x \to y \to y'$ agree. By construction there are surjective maps on objects and morphisms from $\mathcal{S} \to \mathcal{S}'$. We define composition of morphisms in $\mathcal{S}'$ to be the unique law that turns $\mathcal{S} \to \mathcal{S}'$ into a functor. Some details omitted. $\square$

Thus categories fibred in setoids are exactly the categories fibred in groupoids which are equivalent to categories fibred in sets. Moreover, an equivalence of categories fibred in sets is an isomorphism by Lemma 4.38.6.

Lemma 4.39.6. Let $\mathcal{C}$ be a category. The construction of Lemma 4.39.5 part (2) gives a functor

$F : \left\{ \begin{matrix} \text{the 2-category of categories} \\ \text{fibred in setoids over }\mathcal{C} \end{matrix} \right\} \longrightarrow \left\{ \begin{matrix} \text{the category of categories} \\ \text{fibred in sets over }\mathcal{C} \end{matrix} \right\}$

(see Definition 4.29.5). This functor is an equivalence in the following sense:

1. for any two 1-morphisms $f, g : \mathcal{S}_1 \to \mathcal{S}_2$ with $F(f) = F(g)$ there exists a unique 2-isomorphism $f \to g$,

2. for any morphism $h : F(\mathcal{S}_1) \to F(\mathcal{S}_2)$ there exists a 1-morphism $f : \mathcal{S}_1 \to \mathcal{S}_2$ with $F(f) = h$, and

3. any category fibred in sets $\mathcal{S}$ is equal to $F(\mathcal{S})$.

In particular, defining $F_ i \in \textit{PSh}(\mathcal{C})$ by the rule $F_ i(U) = \mathop{\mathrm{Ob}}\nolimits (\mathcal{S}_{i, U})/\cong$, we have

$\mathop{\mathrm{Mor}}\nolimits _{\textit{Cat}/\mathcal{C}}(\mathcal{S}_1, \mathcal{S}_2) \Big/ 2\text{-isomorphism} = \mathop{\mathrm{Mor}}\nolimits _{\textit{PSh}(\mathcal{C})}(F_1, F_2)$

More precisely, given any map $\phi : F_1 \to F_2$ there exists a $1$-morphism $f : \mathcal{S}_1 \to \mathcal{S}_2$ which induces $\phi$ on isomorphism classes of objects and which is unique up to unique $2$-isomorphism.

Proof. By Lemma 4.38.6 the target of $F$ is a category hence the assertion makes sense. The construction of Lemma 4.39.5 part (2) assigns to $\mathcal{S}$ the category fibred in sets whose value over $U$ is the set of isomorphism classes in $\mathcal{S}_ U$. Hence it is clear that it defines a functor as indicated. Let $f, g : \mathcal{S}_1 \to \mathcal{S}_2$ with $F(f) = F(g)$ be as in (1). For each object $U$ of $\mathcal{C}$ and each object $x$ of $\mathcal{S}_{1, U}$ we see that $f(x) \cong g(x)$ by assumption. As $\mathcal{S}_2$ is fibred in setoids there exists a unique isomorphism $t_ x : f(x) \to g(x)$ in $\mathcal{S}_{2, U}$. Clearly the rule $x \mapsto t_ x$ gives the desired $2$-isomorphism $f \to g$. We omit the proofs of (2) and (3). To see the final assertion use Lemma 4.38.6 to see that the right hand side is equal to $\mathop{\mathrm{Mor}}\nolimits _{\textit{Cat}/\mathcal{C}}(F(\mathcal{S}_1), F(\mathcal{S}_2))$ and apply (1) and (2) above. $\square$

Here is another characterization of categories fibred in setoids among all categories fibred in groupoids.

Lemma 4.39.7. Let $\mathcal{C}$ be a category. Let $p : \mathcal{S} \to \mathcal{C}$ be a category fibred in groupoids. The following are equivalent:

1. $p : \mathcal{S} \to \mathcal{C}$ is a category fibred in setoids, and

2. the canonical $1$-morphism $\mathcal{I}_\mathcal {S} \to \mathcal{S}$, see (4.34.2.1), is an equivalence (of categories over $\mathcal{C}$).

Proof. Assume (2). The category $\mathcal{I}_\mathcal {S}$ has objects $(x, \alpha )$ where $x \in \mathcal{S}$, say with $p(x) = U$, and $\alpha : x \to x$ is a morphism in $\mathcal{S}_ U$. Hence if $\mathcal{I}_\mathcal {S} \to \mathcal{S}$ is an equivalence over $\mathcal{C}$ then every pair of objects $(x, \alpha )$, $(x, \alpha ')$ are isomorphic in the fibre category of $\mathcal{I}_\mathcal {S}$ over $U$. Looking at the definition of morphisms in $\mathcal{I}_\mathcal {S}$ we conclude that $\alpha$, $\alpha '$ are conjugate in the group of automorphisms of $x$. Hence taking $\alpha ' = \text{id}_ x$ we conclude that every automorphism of $x$ is equal to the identity. Since $\mathcal{S} \to \mathcal{C}$ is fibred in groupoids this implies that $\mathcal{S} \to \mathcal{C}$ is fibred in setoids. We omit the proof of (1) $\Rightarrow$ (2). $\square$

Lemma 4.39.8. Let $\mathcal{C}$ be a category. The construction of Lemma 4.39.6 which associates to a category fibred in setoids a presheaf is compatible with products, in the sense that the presheaf associated to a $2$-fibre product $\mathcal{X} \times _\mathcal {Y} \mathcal{Z}$ is the fibre product of the presheaves associated to $\mathcal{X}, \mathcal{Y}, \mathcal{Z}$.

Proof. Let $U \in \mathop{\mathrm{Ob}}\nolimits (\mathcal{C})$. The lemma just says that

$\mathop{\mathrm{Ob}}\nolimits ((\mathcal{X} \times _\mathcal {Y} \mathcal{Z})_ U)/\! \cong \quad \text{equals} \quad \mathop{\mathrm{Ob}}\nolimits (\mathcal{X}_ U)/\! \cong \ \times _{\mathop{\mathrm{Ob}}\nolimits (\mathcal{Y}_ U)/\! \cong } \ \mathop{\mathrm{Ob}}\nolimits (\mathcal{Z}_ U)/\! \cong$

the proof of which we omit. (But note that this would not be true in general if the category $\mathcal{Y}_ U$ is not a setoid.) $\square$

[1] A set on steroids!?

In your comment you can use Markdown and LaTeX style mathematics (enclose it like $\pi$). A preview option is available if you wish to see how it works out (just click on the eye in the toolbar).