Joachim's web pages
[Home]
[Math]
[Cat]
Univalence in locally cartesian
closed
∞-categories
By David Gepner and Joachim Kock
ArXiv:1208.1749.
Abstract
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.
Download.
Last updated: 2012-08-09 by
Joachim Kock.