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
Comments (0)