%0 Generic %1 gepner2012univalence %A Gepner, David %A Kock, Joachim %D 2012 %K HoTT category %T Univalence in locally cartesian closed infinity-categories %U http://arxiv.org/abs/1208.1749 %X 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.

@misc{gepner2012univalence, 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 "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 (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 \leq n \leq \infty. 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.}, added-at = {2014-12-14T03:31:45.000+0100}, author = {Gepner, David and Kock, Joachim}, biburl = {https://www.bibsonomy.org/bibtex/2105d3729c3c841189190127e245539c4/t.uemura}, description = {[1208.1749] Univalence in locally cartesian closed infinity-categories}, interhash = {5232b755afe634475f6590e3e634800d}, intrahash = {105d3729c3c841189190127e245539c4}, keywords = {HoTT category}, note = {cite \href{http://arxiv.org/abs/1208.1749}{arxiv:1208.1749}Comment: 26 pages. Comments are very welcome; v2: clarified some points in the introduction, minor expository changes, added one reference. No changes in theorems and proofs}, timestamp = {2014-12-14T03:31:45.000+0100}, title = {Univalence in locally cartesian closed infinity-categories}, url = {http://arxiv.org/abs/1208.1749}, year = 2012 }