Abstract
In the setting of presentable locally cartesian closed infinity-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 infinity-topos has a hierarchy of üniversal" 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 (infinity-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 infinity-category of motivic spaces,
an instance of a locally cartesian closed infinity-category which is not an
n-topos for any 0 n ınfty. Lastly, we show that any presentable
locally cartesian closed infinity-category is modeled by a type-theoretic model
category, and conversely that the infinity-category underlying a type-theoretic
model category is presentable and locally cartesian closed; moreover, univalent
families in presentable locally cartesian closed infinity-categories correspond
precisely to univalent fibrations in type-theoretic model categories.
Description
[1208.1749] Univalence in locally cartesian closed infinity-categories
Links and resources
Tags