Lemma 4.39.4. Let $\mathcal{C}$ be a category. The 2-category of categories fibred in setoids over $\mathcal{C}$ has 2-fibre products. More precisely, the 2-fibre product described in Lemma 4.32.3 returns a category fibred in setoids if one starts out with such.

Proof. Omitted. $\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).