Univalence in locally Cartesian closed categories (Q524707)

This paper is presented by the authors as a complement to the original account of univalence exposed in [\textit{The Univalent Foundations Program}, Homotopy type theory. Univalent foundations of mathematics, Princeton, NJ: Institute for Advanced Study; Raleigh, NC: Lulu Press (2013; Zbl 1298.03002)] The authors start characterizing presentable locally Cartesian closed \(\infty\)-categories as the accessible locally Cartesian localizations of \(\infty\)-topoi. Then they prove: ``For any presentable locally Cartesian closed \(\infty\)-category \(\mathcal {C}\), the equivalence classes of univalent families in \(\mathcal {C}\) form a (possibly large) poset which is canonically isomorphic to the poset of bounded local classes of maps in \(\mathcal {C}\)'', where a bounded local class of maps can be seen as a class of maps which is closed under basechange and satisfies a certain sheaf condition. This result implies that ``in an \(\infty\)-topos, every univalent family is a subfamily of a universal family.'' They show that since any presentable locally Cartesian closed \(\infty\)-category embeds into an \(\infty\)-topos, it follows that every univalent family must be a subfamily of a universal family of the ambient \(\infty\)-topos. Finally, they show a correspondence between presentable locally Cartesian closed \(\infty\)-categories and \(\infty\)-categories underlying a combinatorial type-theoretic model category. ``Under this correspondence, univalent families in presentable locally Cartesian closed \(\infty\)-categories correspond to univalent fibrations in combinatorial type-theoretic model categories.''