pith. the verified trust layer for science. sign in

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

Univalence in locally cartesian closed infinity-categories

classification 🧮 math.CT math.ATmath.LO
keywords univalentcartesianfamilieslocallyclosedinfinity-categoriesinfinity-categorypresentable
0
0 comments X p. Extension
Add this Pith Number to your LaTeX paper What is a Pith Number?
\usepackage{pith}
\pithnumber{ZT4RPDYE}

Prints a linked pith:ZT4RPDYE badge after your title and writes the identifier into PDF metadata. Compiles on arXiv with no extra files. Learn more

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.