Univalence: What It Means Here
Appendix D
Aa
If two types are equivalent, can you substitute one for the other—and with what evidence? The univalence axiom identifies equivalence with equality in a specified type-theoretic universe. This appendix states the axiom and defines transport. Chapter 14 then asks what evidence a receiving operation needs when a deployed evaluator is used for a proposed substitution.
The Univalence Axiom
For types and in a universe , the canonical map is an equivalence. That is: .
An equivalence supplies an identification in the univalent universe. A type family can transport along that path. This does not assert literal equality of external identifiers or unchanged application evaluators; the relevant data move through the identification.
Transport
Given a type family and an identification , transport is the function . It moves data, proofs, and constructions across the identification.
Transport along an identity is supplied by identity elimination without assuming univalence. Univalence supplies an identification from a type equivalence; computation along that identification depends on the foundation. 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 for in a context expecting , you must provide a witnessed equivalence and, for each property the context relies on, an explicit transport certificate that computes the transported property. Within this proposed contract, substitution requires both to be checked for the actual scope, evaluator versions and intended use. A serialized certificate assertion is not its own verification.
| Aspect | Full Univalence | Engineering Univalence (A16) |
|---|---|---|
| Foundation | HoTT / Cubical Type Theory | Practical systems |
| Guarantee | A type equivalence supplies an identification; transport follows by identity elimination | The required property maps and their grounds must be supplied |
| Computation | Constructive settings supply computational rules; axiomatic terms may not reduce | The supplied operation must meet its declared verification and execution contract |
| Requirement | Equivalence witness | Equivalence witness + transport certificates |
| Failure mode | Failure to supply the required typed term | Failed scope or property obligation; missing grounds and unfinished checking remain distinct |
A16 is a proposed engineering discipline inspired by this substitution question, not a machine-checked implementation of the axiom. An implementation can exhibit particular property maps and checks without adopting univalent foundations. Its claim reaches the maps and conditions it actually supplies.