Univalence axiom

For a given universe $U$ , the univalence axiom $u a U$ witnesses that the obvious map

i d t o e q u i v U : (𝐴 \equiv U 𝐵) \to (𝐴 ≃ 𝐵)

is in fact an equivalence. When $U$ has such a witness it is called univalent.¹

#state/develop | #lang/en | #SemBr

Voevodsky borrowed the term from a Russian (mis)translation of faithful as унивалентный. ↩

Footnotes