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.