# Homotopy Type Theory: Univalent Foundations of Mathematics

arXiv: https://arxiv.org/abs/1308.0729 · HTML: https://mlsanity.com/paper/1308.0729/

## Key facts

- Cited by 8 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 3 Aug 2013.

## Built on by (most cited first, 8 of 8)

- [Formal Mathematical Reasoning: A New Frontier in AI](https://mlsanity.com/paper/2412.16075/) (2024)
- [Semantic Search over 9 Million Mathematical Theorems](https://mlsanity.com/paper/2602.05216/) (2026)
- [Artificial Intelligence and the Structure of Mathematics](https://mlsanity.com/paper/2604.06107/) (2026)
- [Improving Autoformalization Using Direct Dependency Retrieval](https://mlsanity.com/paper/2511.11990/) (2025)
- [Evidence-Grounded Verified Agentic Reasoning: A Path Toward Eliminating LLM Hallucination in Empirical Inference via Tool-Attested Kernel Proofs](https://mlsanity.com/paper/2607.12650/) (2026)
- [Semantic Composition in Visually Grounded Language Models](https://mlsanity.com/paper/2305.16328/) (2023)
- [Hey Pentti, We Did It Again!: Differentiable vector-symbolic types that prove polynomial termination](https://mlsanity.com/paper/2510.16533/) (2025)
- [Functorial Neural Architectures from Higher Inductive Types](https://mlsanity.com/paper/2603.16123/) (2026)

## Abstract (arXiv)

Homotopy type theory is a new branch of mathematics, based on a recently discovered connection between homotopy theory and type theory, which brings new ideas into the very foundation of mathematics. On the one hand, Voevodsky's subtle and beautiful "univalence axiom" implies that isomorphic structures can be identified. On the other hand, "higher inductive types" provide direct, logical descriptions of some of the basic spaces and constructions of homotopy theory. Both are impossible to capture directly in classical set-theoretic foundations, but when combined in homotopy type theory, they permit an entirely new kind of "logic of homotopy types". This suggests a new conception of foundations of mathematics, with intrinsic homotopical content, an "invariant" conception of the objects of mathematics -- and convenient machine implementations, which can serve as a practical aid to the working mathematician. This book is intended as a first systematic exposition of the basics of the resulting "Univalent Foundations" program, and a collection of examples of this new style of reasoning -- but without requiring the reader to know or learn any formal logic, or to use any computer proof assistant.