Homotopy type theory

       

Homotopy Type Theory: Univalent Foundations of Mathematics.

•      Homotopy 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 ∞-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 to the 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.

•      In brief, this is another step in the quest to unify all mathematics on consistent foundations. You could say that that project began with the axiomatisation of geometry leading to Euclid’s Elements, and really got going at the start of the 20th century with Russell and Whitehead’s Principia Mathematica, which tried to state everything in terms of sets. Set theory had a huge paradox in the middle of it, so mathematicians have spent the time since Principia trying to come up with something that puts it all on a firm footing. Bourbaki restates all of maths in terms of Zermelo-Fraenkel set theory with the axiom of choice, but some people have serious objections to that too. Meanwhile, category theory and model theory have been providing as much abstraction as anyone can usefully apply, and the advent of computer proof has made constructivism, where you can only accept something exists once you’ve explicitly constructed it, much more popular.

•       Homotopy type theory unifies type theory, arising from logic and computer science, with homotopy theory, which talks about topological spaces. In classical set theory, the base objects are sets, and propositions about those sets exist elsewhere. In homotopy type theory, objects and propositions about objects are instances of the same kind of thing – types – and you can think of types as being spaces of points, which is where the homotopy theory comes in. The philosophy of the book is generously constructivist – they avoid non-constructive concepts like the axiom of choice or law of the excluded middle right up until they need them for things like defining the real numbers.

•      Like Bourbaki, the presentation of these ideas is just as important as the ideas themselves, and the book delivers on that too. The authors have learnt the lesson of Russell and Whitehead, and use notation deftly to avoid losing the reader in a morass of symbols. The introductory sections are short and to the point, giving definitions and justification concisely and clearly. The language is approachable and not at all high-falutin’.