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:

1. 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$,

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

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

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