Joachim's web pages [Home] [Math] [Cat]

Univalence in locally cartesian closed

By David Gepner and Joachim Kock



In the setting of presentable locally cartesian closed ∞-categories, we show that univalent families, in the sense of Voevodsky, form a poset isomorphic to the poset of bounded local classes, in the sense of Lurie. It follows that every ∞-topos has a hierarchy of "universal" univalent families, indexed by regular cardinals, and that n-topoi have univalent families classifying (n-2)-truncated maps. We show that univalent families are preserved (and detected) by right adjoints to locally cartesian localizations, and use this to exhibit certain canonical univalent families in ∞-quasitopoi (∞-categories of "separated presheaves"). We also exhibit some more exotic examples of univalent families, illustrating that a univalent family in an n-topos need not be (n-2)-truncated, as well as some univalent families in the Morel-Voevodsky ∞-category of motivic spaces, an instance of a locally cartesian closed ∞-category which is not an n-topos for any 0 ≤ n ≤ ∞. Lastly, we show that any presentable locally cartesian closed ∞-category is modeled by a type-theoretic model category, and conversely that the ∞-category underlying a type-theoretic model category is presentable and locally cartesian closed; moreover, univalent families in presentable locally cartesian closed ∞-categories correspond precisely to univalent fibrations in type-theoretic model categories.


Last updated: 2012-08-09 by Joachim Kock.