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$

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).