Fibre category

Consider a displayed category $𝖣 ⇥ 𝖢$ . For each $𝑎 \in 𝖢 0$ , the fibre category $𝖣 𝑎$ is an ordinary category where #m/def/cat/dis

an object is an object displayed over $𝑎$ , i.e. $(𝖣 𝑎) 0 = 𝖣 𝑎$ ;
a morphism is a morphism displayed over $i d 𝑎$ , i.e. $𝖣 𝑎 (𝑥, 𝑦) = 𝖣 [i d 𝑎] (𝑥, 𝑦)$ .

Morphisms in fibre categories are called vertical since they do not cross between fibres.

In this way a displayed category $𝖣 ⇥ 𝖢$ gives a $𝖢 0$ -indexed family of categories. However, this need not be functorial, see Cartesian fibration.

#state/tidy | #lang/en | #SemBr