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)