Homotopy Type Theory and Univalence

In ordinary mathematical prose, equality often appears as a yes-or-no relationship. In intensional type theory, an equality is represented by an identity type, and that type can itself have mathematical structure.

Homotopy type theory investigates this structure through connections with topology and higher-dimensional mathematics. Univalent foundations develop a related account of when equivalent objects can be identified.

This is a particular foundational research program. It is not a feature automatically shared by every dependent-type proof assistant.

Returning to identity types

The dependent-type note introduced

the type of identifications between $a$ and $b$ in $A$.

Reflexivity supplies an identification of $a$ with itself. Identity elimination supports constructions such as symmetry, transitivity, and transport along equality.

The rules of intensional type theory do not generally force all proofs of an identity to be identical. Whether such uniqueness can be derived is a mathematical question about the theory.

Martin Hofmann and Thomas Streicher's groupoid interpretation, presented in 1994 and developed further afterward, showed that uniqueness of identity proofs is not generally derivable in the relevant intensional setting.

Their model gave objects and identifications a structured interpretation. It provided an important precursor to the higher-dimensional viewpoint.

The path interpretation

Think of a type as a space and an identity between its elements as a path. A path between paths then represents an identity between identifications.

This picture is a guide to formal structure. It does not mean that every type is literally defined as a subset of Euclidean space or that every proof is an ordinary drawn curve.

Steve Awodey and Michael Warren developed homotopy-theoretic interpretations of identity types. Vladimir Voevodsky's work on simplicial models and univalence supplied another central strand.

The developments connected type theory with structures already studied in homotopy theory: points, paths, homotopies, and their higher relationships.

The connection changes the questions one can ask. Instead of assuming that all self-identifications are indistinguishable, one can study a type's loops and higher identity structure.

Transport as a concrete operation

Let $P:A\to\mathcal U$ be a family of types. If $p:a=b$ and $u:P(a)$, identity elimination gives

For a familiar example, suppose $A=\mathbb N$ and $P(n)=\operatorname{Vec}(X,n)$. An equality between two lengths permits a vector to be regarded at the corresponding equal index.

Transport along reflexivity computes to the original term. For a more general identity, the operation records how the dependent information moves.

In the geometric interpretation, a family behaves like varying data over points of a base, and transport follows a path in that base. The formal rules and the picture reinforce one another, provided their levels are kept distinct.

Equivalence of types

A function $f:A\to B$ is an equivalence when it has the appropriate invertibility property. One formulation says that each fiber

is contractible: it has a specified center and every element can be identified with that center.

This formulation includes coherence in a way suitable for higher identity. Merely writing two inverse-looking functions without stating the required equalities would leave the definition incomplete.

Write $A\simeq B$ for the type of equivalences.

An identification $A=B$ in a universe always induces an equivalence, by identity elimination:

Reflexivity induces the identity equivalence. The question is whether every equivalence arises in this way with the appropriate uniqueness structure.

The univalence axiom

Univalence asserts that the canonical map from identifications to equivalences is itself an equivalence:

It makes precise a form of reasoning in which equivalent types can be identified within a universe.

This is stronger and more structured than the informal instruction to “treat isomorphic objects as the same.” It specifies how identity in the universe relates to equivalence and how dependent constructions respect it.

For example, a bijection between two finite sets can provide an identification of their underlying types in a suitable univalent setting. Transport then carries constructions expressed over those types.

If the objects also have operations, a bare equivalence of carrier types does not automatically preserve those operations. A group isomorphism must respect multiplication and the other structure. Structure-identity principles extend the analysis with such conditions.

The additional structure is what permits mathematical statements to transfer correctly.

A circle with a specified loop

A higher inductive type can specify both point constructors and path constructors.

The circle is described informally by a point

and a loop

The associated elimination principle says what data are needed to define a map out of the circle: an image point and a compatible loop at that point, with the appropriate computation rules.

The loop is not imposed as equal to reflexivity. In the developed theory, the loop space of the circle can be related to the integers, with winding around the circle corresponding to positive and negative iterations.

That statement requires a substantial proof, commonly organized through an encode–decode method. The two constructor declarations alone do not prove the calculation.

The example shows why higher identity is mathematically useful. A type can present a space through generators and identifications rather than encoding every construction indirectly in a set-theoretic representation.

The collaborative development of HoTT

The 2012–2013 special year at the Institute for Advanced Study brought together researchers working on type theory, homotopy, and univalent foundations.

The resulting Homotopy Type Theory: Univalent Foundations of Mathematics was a collaborative 2013 book, developed through an unusually open writing process.

Its organization moves from type-theoretic foundations to homotopy theory, set-level mathematics, and other applications. The book is an important synthesis, not the beginning of every idea it presents.

Contributors and antecedents matter because the field combined several mathematical traditions. Assigning the entire development to a single theorem prover or a single publication would obscure its substance.

Why computation became a new problem

Adding an axiom to a type theory may provide new proofs without providing reduction rules for the new constants.

For univalence and higher inductive constructions, researchers wanted a computational account compatible with the constructive aims of type theory. A proof involving transport should ideally support meaningful evaluation, with appropriate normalization or canonicity results.

Cubical approaches use interval-like dimensions and operations on higher-dimensional objects. Work by Marc Bezem, Thierry Coquand, Simon Huber, and others developed models; Cyril Cohen, Coquand, Huber, and Anders Mörtberg presented an influential cubical type theory.

Their paper provides a constructive treatment in which univalence is supported by the theory's computational structure. Related work establishes canonicity results and extends the treatment of higher inductive types.

The precise result depends on the particular cubical calculus. “Cubical” names a family of approaches, not a single interchangeable implementation.

What this does and does not imply for assistants

Ordinary Lean foundations do not adopt univalence as their default account of identity. Coq/Rocq, Agda, and other ecosystems support different libraries, extensions, or specialized modes with their own rules.

A claim that a theorem has been checked must therefore specify the system and assumptions. A theorem in a HoTT library and a theorem in an ordinary classical higher-order or proof-irrelevant dependent theory may rest on different foundations.

HoTT also does not replace all earlier proof theory, set theory, or categorical logic. It creates new connections and new foundational possibilities while leaving those fields with their own questions.

From foundations to learned proof search

The type system determines what counts as an acceptable proof. The process of finding such a proof can use many different methods, including statistical prediction.

The final main note examines how learned systems interact with formal libraries and checkers, and why successful search must still be distinguished from faithful formalization and new mathematical discovery.

Sources and further reading

• Martin Hofmann and Thomas Streicher, “The Groupoid Model Refutes Uniqueness of Identity Proofs” (1994); “The Groupoid Interpretation of Type Theory” (1998).
• Steve Awodey and Michael A. Warren, “Homotopy Theoretic Models of Identity Types” (2009).
• The Univalent Foundations Program, Homotopy Type Theory: Univalent Foundations of Mathematics (2013).
• Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg, “Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom”, preprint 2016, proceedings publication 2018.
• Simon Huber, “Canonicity for Cubical Type Theory” (2016 preprint).
• Marc Bezem, Thierry Coquand, and Simon Huber, “The Univalence Axiom in Cubical Sets” (2017 preprint).