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

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

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

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.

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}$.

## Comments (0)