Equality with structure
An inhabitant $p : x =_A y$ witnesses an identification between two terms. Identity elimination supplies composition and inverses up to higher identifications; these laws need not hold judgmentally.
The resulting hierarchy motivates a groupoid interpretation of types: objects are terms, morphisms are identifications, and higher morphisms witness coherence.
The universe matters
Univalence identifies equivalences with paths in a universe, through the statement $(A \simeq B) \simeq (A =_{\mathcal{U}} B)$. It does not make every judgmental equality decidable or erase the distinction between syntax and semantics.
For a complete treatment, consult The HoTT Book, especially its chapters on identity types and univalence.
An implementation stores LaTeX literally: \mathcal{U}, \simeq, \infty.
Code fences are never mathematical rendering targets.This original editorial primer is an orientation, not a peer-reviewed research claim.