Universes, univalence, and homotopy type theory

In the predicative hierarchy used here, each universe belongs to a strictly larger universe. A small family has a specified domain level and fiber level; forming its dependent sum or product normally uses the maximum of those levels. One may choose a cumulative formulation, allowing a small type to be regarded at higher levels, but that is an explicit rule of the theory. It does not turn a universe into an element of itself.

The collection of small types is larger than an individual small type. Likewise, collecting all small mere propositions can raise a universe level, even though each proposition is individually small. Resizing principles can change such bookkeeping, but they are additional assumptions and are not automatic consequences of calling a type a proposition. A formal statement about all types must therefore say which universe it quantifies over instead of hiding an unrestricted self-containing collection behind informal notation.

Path induction always sends an identity between two types to an equivalence: transport along reflexivity is the identity equivalence, and the construction extends to all paths. Univalence asserts that this canonical map is itself an equivalence. Its inverse assigns a universe path to an equivalence. For general types, equivalence means a map with contractible fibers or an equivalent standard formulation, not merely a bijection between visible points that ignores higher identity information.

A consequence is that transporting an element along the path associated to an equivalence agrees propositionally with applying the equivalence. This agreement follows from the inverse laws for the canonical map and can be used as an internal equality proof. Univalence also entails function extensionality in the standard setting of the cited book. It does not say that every path is judgmentally reflexivity, or that arbitrary equivalences become syntactically identical terms in a checker.

Ordinary intensional type theory can postulate a constant expressing univalence. With no corresponding reduction equations, a transport term involving that constant may remain stuck even when its expected result is propositionally known. This need not refute logical consistency; it means the original operational rules do not supply the desired computation. One must distinguish semantic justification of an axiom, internal proof consequences, and a normalization algorithm for extended syntax.

Cohen, Coquand, Huber, and Mörtberg instead give a cubical calculus with interval names, composition, and glueing operations in which univalence is provable with computational content. Huber's separate canonicity theorem establishes the stated numeral result for that particular calculus. These are precise developments, not a license to attach the same theorems to every language called homotopy type theory. Adding further higher inductive types, rewrite rules, or axioms calls for the corresponding computational and consistency analysis.