Lemma 4.38.6. Let $\mathcal{C}$ be a category. The construction of Lemma 4.38.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.28.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{Mor}\nolimits _{\textit{Cat}/\mathcal{C}}(\mathcal{S}_1, \mathcal{S}_2) \Big/ 2\text{-isomorphism} = \mathop{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.37.6 the target of $F$ is a category hence the assertion makes sense. The construction of Lemma 4.38.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.37.6 to see that the right hand side is equal to $\mathop{Mor}\nolimits _{\textit{Cat}/\mathcal{C}}(F(\mathcal{S}_1), F(\mathcal{S}_2))$ and apply (1) and (2) above. $\square$

## Post a comment

Your email address will not be published. Required fields are marked.

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

Unfortunately JavaScript is disabled in your browser, so the comment preview function will not work.

All contributions are licensed under the GNU Free Documentation License.

In order to prevent bots from posting comments, we would like you to prove that you are human. You can do this by filling in the name of the current tag in the following input field. As a reminder, this is tag 04SC. Beware of the difference between the letter 'O' and the digit '0'.