Lemma 4.39.8. Let $\mathcal{C}$ be a category. The construction of Lemma 4.39.6 which associates to a category fibred in setoids a presheaf is compatible with products, in the sense that the presheaf associated to a $2$-fibre product $\mathcal{X} \times _\mathcal {Y} \mathcal{Z}$ is the fibre product of the presheaves associated to $\mathcal{X}, \mathcal{Y}, \mathcal{Z}$.
Proof. Let $U \in \mathop{\mathrm{Ob}}\nolimits (\mathcal{C})$. The lemma just says that
\[ \mathop{\mathrm{Ob}}\nolimits ((\mathcal{X} \times _\mathcal {Y} \mathcal{Z})_ U)/\! \cong \quad \text{equals} \quad \mathop{\mathrm{Ob}}\nolimits (\mathcal{X}_ U)/\! \cong \ \times _{\mathop{\mathrm{Ob}}\nolimits (\mathcal{Y}_ U)/\! \cong } \ \mathop{\mathrm{Ob}}\nolimits (\mathcal{Z}_ U)/\! \cong \]
the proof of which we omit. (But note that this would not be true in general if the category $\mathcal{Y}_ U$ is not a setoid.) $\square$
Comments (0)