It is expected that every (infinity,1)-topos? admits a model of homotopy type theory with the univalence axiom and higher inductive types. However, this has not been completely proven for the sort of univalent universes in common use.
Revision on February 18, 2014 at 12:42:18 by Mike Shulman. See the history of this page for a list of all contributions to it.