The Living Thing / Notebooks : Foundations of mathematics

This is a long story which I will not attempt to tell here; ZFC set theory (“Zermelo–Fraenkel plus axiom of choice”) and its relatives are the default foundations for mathematics used by working mathematicians, and they are certainly better than no foundations. They have many irritating features, however, such as tying up armies of mathematicians in endless arguments about the Axiom of Choice, and leaving people such as me who do measure theory spending far too much time on the pathologies of set theory in infinite limits because of said axiom.

If one is dissatisfied with this state of affairs, one can do several different things: One can come up with variations on the theme of axiom of choice, which is a great way of starting especially smug arguments from partisans of each side, or one can throw the whole set theoretic basis out and try something different, such as category-theory-esque Type theory.

The latter sounds much more satisfying to someone of my temper.

Will I ever have justification for spending time on realy understanding these, however? Doubtful. Unmeasurable sets don’t plague me every day, and the foundations work if you sweep the cantor dust under the carpet. It’s still unsatisfying though, so just in case I’ll record some stuff here…

Vladimir Voevodsky and friends’ Homotopy Type Theory (HoTT to its friends):

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 offers a new “univalent” foundation of mathematics, in which a central role is played by Voevodsky’s univalence axiom and higher inductive types. 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.

David McAllester’s Morphoid Type Theory


Mazur, B. (2007) When is one thing equal to some other thing?. In B. Gold & R. A. Simons (Eds.), Proof and Other Dilemmas: Mathematics and Philosophy (p. 221). Washington, D.C.: Mathematical Association of America
McAllester, D. (2014a) Implementation and Abstraction in Mathematics. arXiv:1407.7274 [cs].
McAllester, D. (2014b) Morphoid Type Theory. arXiv:1407.7274 [cs].
Program, T. U. F.(2013) Homotopy Type Theory: Univalent Foundations of Mathematics. . Institute for Advanced Study:
Rijke, E. (2012) Homotopy type theory.