Computational Interpretation of Univalent Homotopy Type Theory

Definitions and mathematical statement

For a type $A$ and terms $a,b:A$, write $\operatorname{Id}_A(a,b)$ for the identity type expressing equality of $a$ and $b$. For types $A,B$, write $\operatorname{Equiv}(A,B)$ for the type of equivalences between them. In the usual formulation, univalence for a universe $\mathcal U$ asserts that, for every $A,B:\mathcal U$, the canonical map \[ \operatorname{idtoequiv}_{A,B}:\operatorname{Id}_{\mathcal U}(A,B)\longrightarrow\operatorname{Equiv}(A,B) \] is an equivalence. This notation explains the named axiom; it does not specify a universe hierarchy or a complete underlying type theory, neither of which is fixed by the supplied record.

Conjecture (source formulation, 2011). All axioms of homotopy type theory, including univalence, admit a computational interpretation obtained by defining equality on a type recursively on that type, extending Gandy's interpretation for simple type theory.

Unresolved qualifications. This is a schematic conjecture rather than a fully specified formal existence statement. The supplied record does not fix the syntax, type constructors, universe rules, or collection of axioms quantified over by "all axioms of homotopy type theory." It also does not specify the target computational formalism, the clauses and admissible recursion principle for defining equality, the distinction between judgmental equality and identity types in that construction, or the precise computational and preservation properties required of an interpretation. The particular formulation of Gandy's interpretation to be extended and the meaning of extension are likewise unspecified. These choices require clarification before a precise formal proposition can be extracted; the displayed univalence schema alone does not resolve them.

Short English statement

The conjecture asks whether equality can be interpreted recursively in the structure of types so as to give a computational interpretation of every axiom of homotopy type theory, including univalence, extending Gandy's interpretation of simple type theory. The underlying theory and the required computational properties remain unspecified. The supplied record labels the problem partially solved; this draft does not independently verify that assessment.

Sources

• Local UnsolvedMath registry, permanent ID $30001722$, source problem code catalogue entry, title "Computational Interpretation of Univalent Homotopy Type Theory," in the collection "Oberwolfach Reports Open Problems." The supplied record dates the conjecture to 2011 and names no individual proposer.
• Mini-Workshop: The Homotopy Interpretation of Constructive Type Theory (2011), Oberwolfach Reports, pp. 609--638, DOI 10.4171/owr/2011/11. Supplied source report and literature reference "Oberwolfach Report 11/2011": https://doi.org/10.4171/owr/2011/11. The collection describes these reports as documenting mathematical workshops and their open-problem discussions. The supplied record marks the statement corrected_verified and reports that the official report confirms the conjecture, with only the extraction label removed; this verification claim has not been independently checked here.
• Supplied literature reference "Barras--Coquand--Huber": https://ncatlab.org/nlab/files/BarrasCoquandHuber-TakeutiGandyInterpretation.pdf. No further bibliographic details or theorem-level correspondence are supplied.
• Supplied literature assessment, checked 2026-08-21: status "partially solved." The assessment states that generalized Takeuti--Gandy style computational interpretations and formal developments exist, but that the report's conjecture for all univalence-related equality axioms by recursion on types is not established in full. This is supplied dated curation derived from the Oberwolfach Reports collection, not an independently verified literature assessment. Its time-sensitive status and cited claims require independent verification.