Comprehension schemes arose as crucial notions in the early work on the foundations of set theory, and hence they found expression in a considerable variety of foundational settings for mathematics. Particularly, they have been introduced to the context of categorical logic first by Lawvere and then by Benabou in the 1970s.
In this talk we define and study a theory of comprehension schemes for fibered ∞-categories, generalizing Johnstone’s respective notion for ordinary categories. This includes natural generalizations of all the fundamental instances originally defined by Benabou, and their application to Jacob’s comprehension categories. Thereby, we can characterize
- numerous categorical structures arising in higher topos theory,
- the notion of univalence,
- internal ∞-categories,
in terms of comprehension schemes, while some of the 1-categorical counterparts fail to hold in ordinary category theory. As an application, we can show that the universal cartesian fibration is represented via externalization by the “freely walking chain” in the ∞-category of small ∞-categories.
In the end, if my time management permits, we take a look at the externalization construction of internal ∞-categories from a model categorical perspective and review some examples from the literature in this light.
This video is part of Masaryk University‘s Algebra seminar.
