pith. machine review for the scientific record. sign in

arxiv: 1208.1749 · v5 · submitted 2012-08-08 · 🧮 math.CT · math.AT· math.LO

Recognition: unknown

Univalence in locally cartesian closed infinity-categories

Authors on Pith no claims yet
classification 🧮 math.CT math.ATmath.LO
keywords univalentcartesianfamilieslocallyclosedinfinity-categoriesinfinity-categorypresentable
0
0 comments X
read the original abstract

After developing the basic theory of locally cartesian localizations of presentable locally cartesian closed infinity-categories, we establish the representability of equivalences and 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 infinity-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 infinity-quasitopoi (certain infinity-categories of "separated presheaves", introduced here). 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 infinity-category of motivic spaces, an instance of a locally cartesian closed infinity-category which is not an n-topos for any $0\leq n\leq\infty$. Lastly, we show that any presentable locally cartesian closed infinity-category is modeled by a combinatorial type-theoretic model category, and conversely that the infinity-category underlying a combinatorial type-theoretic model category is presentable and locally cartesian closed. Under this correspondence, univalent families in presentable locally cartesian closed infinity-categories correspond to univalent fibrations in combinatorial type-theoretic model categories.

This paper has not been read by Pith yet.

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.