Comprehension categories and the semantics of type dependency (Q1208414)

A comprehension category is a functor \({\mathcal P} : \mathbb{E} \to \mathbb{B}^ \to\) such that (i) \(cod \circ {\mathcal P} : \mathbb{E} \to \mathbb{B}\) is a fibration, and (ii) \(f\) is cartesian in \(\mathbb{E}\) implies that \({\mathcal P}f\) is a pullback in \(\mathbb{B}\). Here \(\mathbb{B}^ \to\) is the arrow category of \(\mathbb{B}\), and \(cod : \mathbb{B}^{\to}\to \mathbb{B}\) is the codomain functor. The author starts with a presentation of the basic facts about fibrations and fibered adjunctions due to A. Grothendieck and J. Bénabou. The paper is mainly devoted to the discussion of numerous examples of comprehension categories. It is shown that many categorical structures introduced by various authors to describe type dependency are particular cases of the general notion of a comprehension category. Examples include, among others, term model, display-map categories, topos comprehension, categories with attributes, Ehrhard's \(D\)-categories, family models, Lawvere's hyperdoctrines, Pavlović's comprehension. Closed comprehension categories are also discussed.