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$

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