Univalence: What It Means Here

Appendix D

2 min read

Univalence: What It Means Here

If two types are equivalent, can you substitute one for the other—and with what evidence? The univalence axiom gives the strongest possible answer. This appendix states the axiom, defines transport, and explains why the main text uses a weaker engineering version.

The Univalence Axiom

Univalence Axiom

For types $A$ and $B$ in a universe $\mathcal{U}$ , the canonical map $\mathsf{idtoeqv} : (A = B) \to (A \simeq B)$ is an equivalence. That is: $(A \simeq B) \simeq (A = B)$ .

Equivalence of types is equality of types. If you exhibit $e : A \simeq B$ , then $A$ and $B$ are identical for all purposes: anything proved about $A$ holds automatically for $B$ .

Transport

Given a type family $P : \mathcal{U} \to \mathcal{U}$ and an identification $p : A = B$ , transport is the function $\mathsf{transport}^P(p) : P(A) \to P(B)$ . It moves data, proofs, and constructions across the identification.

Univalence guarantees that transport exists; it does not always tell you how to compute it. In axiomatic HoTT, some transported terms are "stuck" (they have the right type but don't reduce to canonical forms). Cubical type theory solves this by making transport a definable operation. The main text does not assume computational univalence.

Engineering Univalence (A16)

To substitute $B$ for $A$ in a context expecting $A$ , you must provide a witnessed equivalence $e : A \simeq B$ and, for each property $P$ the context relies on, an explicit transport certificate $\tau_P : P(A) \to P(B)$ that computes the transported property. Substitution is valid if and only if both are exhibited.

Aspect	Full Univalence	Engineering Univalence (A16)
Foundation	HoTT / Cubical Type Theory	Practical systems
Guarantee	Transport always exists	Transport must be exhibited
Computation	Computes (cubical) / may be stuck (axiomatic)	Always computes (by construction)
Requirement	Equivalence witness	Equivalence witness + transport certificates
Failure mode	Type error	Missing certificate (specific property)

Engineering univalence is weaker than full univalence but implementable today. Witnesses are already required (A10), certificates are auditable, and failures are localized to specific missing properties. The discipline: don't claim equivalence implies substitutability—exhibit the mechanism.

← Back to Appendices Back to The Proofs →