Homotopy Type Theory: Univalent Foundations of MathematicsHomotopy type theory is a new branch of mathematics that combines aspects of several different fields in a surprising way. It is based on a recently discovered connection between homotopy theory and type theory. It touches on topics as seemingly distant as the homotopy groups of spheres, the algorithms for type checking, and the definition of weak $\infty$-groupoids. Homotopy type theory brings new ideas into the very foundation of mathematics. On the one hand, there is Voevodsky's subtle and beautiful univalence axiom. The univalence axiom implies, in particular, that isomorphic structures can be identified, a principle that mathematicians have been happily using on workdays, despite its incompatibility with the "official" doctrines of conventional foundations. On the other hand, we have higher inductive types, which provide direct, logical descriptions of some of the basic spaces and constructions of homotopy theory: spheres, cylinders, truncations, localizations, etc. Both ideas 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 tothe working mathematician. This is the Univalent Foundations program. The present book is intended as a first systematic exposition of the basics of univalent foundations, 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. We believe that univalent foundations will eventually become a viable alternative to set theory as the "implicit foundation" for the unformalized mathematics done by most mathematicians. |
What people are saying - Write a review
User Review - Flag as inappropriate
The pdf of this book is available at: http://homotopytypetheory.org/book/
The source code, including Coq proofs, is at: https://github.com/HoTT/book
If you have a correction or improvement, please contribute.
Common terms and phrases
algebraic apply assume axiom of choice cartesian product category theory Cauchy approximation Cauchy reals Cauchy sequences Chapter characterization classical codomain colimits composite computation rule construct contractible coproduct Corollary Dedekind reals defining equations denote dependent function element equivalence relation example excluded middle Exercise fiber fibration function extensionality function f function type functor give given groupoid hence higher inductive types homotopy groups homotopy theory homotopy type theory identity types implies induction principle inductive definition inductive hypothesis inhabited instance inverse isomorphism judgmental equality Lemma logic mathematics merely exists morphisms n-connected n-truncated n-type natural numbers notation notion pair path induction precategory Proof Prop propositional truncation prove pushout quasi-inverse quotient rat(q rat(r real numbers recursion recursion principle refla reflx sequence set theory Similarly structure suffices to show Suppose surjective Theorem topological type family uniqueness principle univalence univalence axiom univalent foundations universal property
Bibliographic information
| Title | Homotopy Type Theory: Univalent Foundations of Mathematics |
| Author | Univalent Foundations Program |
| Editor | Univalent Foundations Program |
| Contributor | Institute for Advanced Study (Princeton, N.J.) |
| Publisher | Univalent Foundations, 2013 |
| Length | 595 pages |
| Export Citation | BiBTeX EndNote RefMan |