The Stacks project

Proof. Assume $p : \mathcal{S} \to \mathcal{C}$ is fibred in groupoids. To show all fibre categories $\mathcal{S}_ U$ for $U \in \mathop{\mathrm{Ob}}\nolimits (\mathcal{C})$ are groupoids, we must exhibit for every $f : y \to x$ in $\mathcal{S}_ U$ an inverse morphism. The diagram on the left (in $\mathcal{S}_ U$) is mapped by $p$ to the diagram on the right:

Since only $\text{id}_ U$ makes the diagram on the right commute, there is a unique $g : x \to y$ making the diagram on the left commute, so $fg = \text{id}_ x$. By a similar argument there is a unique $h : y \to x$ so that $gh = \text{id}_ y$. Then $fgh = f : y \to x$. We have $fg = \text{id}_ x$, so $h = f$. Condition (2) of Definition 4.35.1 says exactly that every morphism of $\mathcal{S}$ is strongly cartesian. Hence condition (1) of Definition 4.35.1 implies that $\mathcal{S}$ is a fibred category over $\mathcal{C}$.

Conversely, assume all fibre categories are groupoids and $\mathcal{S}$ is a fibred category over $\mathcal{C}$. We have to check conditions (1) and (2) of Definition 4.35.1. The first condition follows trivially. Let $\phi : y \to x$, $\psi : z \to x$ and $f : p(z) \to p(y)$ such that $p(\phi ) \circ f = p(\psi )$ be as in condition (2) of Definition 4.35.1. Write $U = p(x)$, $V = p(y)$, $W = p(z)$, $p(\phi ) = g : V \to U$, $p(\psi ) = h : W \to U$. Choose a strongly cartesian $g^*x \to x$ lying over $g$. Then we get a morphism $i : y \to g^*x$ in $\mathcal{S}_ V$, which is therefore an isomorphism. We also get a morphism $j : z \to g^*x$ corresponding to the pair $(\psi , f)$ as $g^*x \to x$ is strongly cartesian. Then one checks that $\chi = i^{-1} \circ j$ is a solution.

We have seen in the proof of (1) $\Rightarrow $ (2) that every morphism of $\mathcal{S}$ is strongly cartesian. The final statement follows directly from Lemma 4.33.7. $\square$