Univalent category

A univalent category¹ $𝖢 0$ is a category such that the canonical map

i d t o i s o 𝖢 : (𝐴 \equiv 𝖢 0 𝐵) \to (𝐴 ≅ 𝖢 𝐵)

is an equivalence. Such categories make it impossible to disrespect the principle of equivalence.

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

When working in Univalent Foundations it is traditional to call a univalent category a category, with the ordinary notion downgraded to precategory. ↩

Footnotes