Univalence in locally cartesian closed infinity-categories
I'll explain the meaning of univalence in the setting of
presentable locally cartesian closed infinity-categories.
Univalent families correspond precisely to bounded local classes
of maps in the sense of Lurie. Lurie shows that locality of
the class of all maps is equivalent to the infinity-topos axiom.
To exhibit large univalent families outside the realm of
toposes, we introduce notions of infinity-quasitoposes, as
certain infinity-categories of separated presheaves, sitting
in between two infinity-toposes, and show that the map classifier
in the small topos induces a univalent family in the quasi-topos.
This is joint work with David Gepner.