Lemma 8.2.5. Let $\mathcal{C}$ be a category. Let $p : \mathcal{S} \to \mathcal{C}$ be a fibred category, see Categories, Section 4.33. Let $U \in \mathop{\mathrm{Ob}}\nolimits (\mathcal{C})$ and let $x, y \in \mathop{\mathrm{Ob}}\nolimits (\mathcal{S}_ U)$. Denote $x, y : \mathcal{C}/U \to \mathcal{S}$ also the corresponding $1$-morphisms, see Categories, Lemma 4.41.2. Then

1. the $2$-fibre product $\mathcal{S} \times _{\mathcal{S} \times \mathcal{S}, (x, y)} \mathcal{C}/U$ is fibred in setoids over $\mathcal{C}/U$, and

2. $\mathit{Isom}(x, y)$ is the presheaf of sets corresponding to this category fibred in setoids, see Categories, Lemma 4.39.6.

Proof. Omitted. Hint: Objects of the $2$-fibre product are $(a : V \to U, z, (\alpha , \beta ))$ where $\alpha : z \to a^*x$ and $\beta : z \to a^*y$ are isomorphisms in $\mathcal{S}_ V$. Thus the relationship with $\mathit{Isom}(x, y)$ comes by assigning to such an object the isomorphism $\beta \circ \alpha ^{-1}$. $\square$

Comment #7555 by Jiangfan on

There are two $a:V \to U$ in the object of the 2-fibre product, one of them should be redundant?

There are also:

• 2 comment(s) on Section 8.2: Presheaves of morphisms associated to fibred categories

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