Lemma 4.39.6. Let $\mathcal{C}$ be a category. The construction of Lemma 4.39.5 part (2) gives a functor
\[ F : \left\{ \begin{matrix} \text{the 2-category of categories}
\\ \text{fibred in setoids over }\mathcal{C}
\end{matrix} \right\} \longrightarrow \left\{ \begin{matrix} \text{the category of categories}
\\ \text{fibred in sets over }\mathcal{C}
\end{matrix} \right\} \]
(see Definition 4.29.5). This functor is an equivalence in the following sense:
for any two 1-morphisms $f, g : \mathcal{S}_1 \to \mathcal{S}_2$ with $F(f) = F(g)$ there exists a unique 2-isomorphism $f \to g$,
for any morphism $h : F(\mathcal{S}_1) \to F(\mathcal{S}_2)$ there exists a 1-morphism $f : \mathcal{S}_1 \to \mathcal{S}_2$ with $F(f) = h$, and
any category fibred in sets $\mathcal{S}$ is equal to $F(\mathcal{S})$.
In particular, defining $F_ i \in \textit{PSh}(\mathcal{C})$ by the rule $F_ i(U) = \mathop{\mathrm{Ob}}\nolimits (\mathcal{S}_{i, U})/\cong $, we have
\[ \mathop{\mathrm{Mor}}\nolimits _{\textit{Cat}/\mathcal{C}}(\mathcal{S}_1, \mathcal{S}_2) \Big/ 2\text{-isomorphism} = \mathop{\mathrm{Mor}}\nolimits _{\textit{PSh}(\mathcal{C})}(F_1, F_2) \]
More precisely, given any map $\phi : F_1 \to F_2$ there exists a $1$-morphism $f : \mathcal{S}_1 \to \mathcal{S}_2$ which induces $\phi $ on isomorphism classes of objects and which is unique up to unique $2$-isomorphism.
Proof.
By Lemma 4.38.6 the target of $F$ is a category hence the assertion makes sense. The construction of Lemma 4.39.5 part (2) assigns to $\mathcal{S}$ the category fibred in sets whose value over $U$ is the set of isomorphism classes in $\mathcal{S}_ U$. Hence it is clear that it defines a functor as indicated. Let $f, g : \mathcal{S}_1 \to \mathcal{S}_2$ with $F(f) = F(g)$ be as in (1). For each object $U$ of $\mathcal{C}$ and each object $x$ of $\mathcal{S}_{1, U}$ we see that $f(x) \cong g(x)$ by assumption. As $\mathcal{S}_2$ is fibred in setoids there exists a unique isomorphism $t_ x : f(x) \to g(x)$ in $\mathcal{S}_{2, U}$. Clearly the rule $x \mapsto t_ x$ gives the desired $2$-isomorphism $f \to g$. We omit the proofs of (2) and (3). To see the final assertion use Lemma 4.38.6 to see that the right hand side is equal to $\mathop{\mathrm{Mor}}\nolimits _{\textit{Cat}/\mathcal{C}}(F(\mathcal{S}_1), F(\mathcal{S}_2))$ and apply (1) and (2) above.
$\square$
Comments (0)