Homotopy Type Theory: Univalent Foundations of Mathematics

By The Univalent Foundations Program. arXiv.org, 2013

502 citations recorded by the source corpus.

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.

View Paper: https://www.semanticscholar.org/paper/bdd73e7047e4dddcec4757146d014b45566c251b

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

1. Vladimir Voevodsky
2. Krzysztof Kapulkin
3. Anders Mörtberg
4. Peter LeFanu Lumsdaine
5. Soonho Kong
6. Thierry Coquand
7. C. Cohen
8. Jeremy Avigad

Citations in the corpus

• The simplicial model of Univalent Foundations (after Voevodsky) (2012, unknown): “In particular, the analogue of Lemma 3.3.4 for homotopy equivalences does not hold; for further discussion of these issues, see [Uni13, Ch. 4].”
• Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom (2015, background): “This paper presents two main contributions.”
• The Lean Theorem Prover (System Description) (2015, methodology): “Lean also contains a library tailored for Homotopy Type Theory (HoTT) [23], using a predicative and proof relevant instantiation of the kernel.”
• THE SIMPLICIAL MODEL OF UNIVALENT FOUNDATIONS (2014, background): “In the language of [Uni13], it is a mere proposition.”
• An experimental library of formalized Mathematics based on the univalent foundations (2015, methodology): “The proper solution is instead to use universe polymorphism together with either resizing rules (see Voevodsky 2011) or higher inductive types (see Univalent Foundations Project 2013).”