A univalent type theory is a homotopy type theory with universes such that all universes are univalent universes.
Revision on May 1, 2022 at 19:40:10 by Anonymous?. See the history of this page for a list of all contributions to it.