New foundations?

This I find intriguing:

Can we actually use [homotopy] type theory as the foundation for mathematics? That is, must we consider the objects of mathematics to “really” be built out of sets, with “types” just a convenient fiction for talking about such structures? Or can we consider types to be the basic objects of mathematics, with everything else built out of them?

The answer is undoubtedly yes: the “sets” in type theory can encode mathematics just like the sets of ZFC can.

The real question, therefore, is not “can we?” but “should we?” This is where things get more philosophical. Over the past century, mathematicians and philosophers have become accustomed to the fundamental objects of mathematics being discrete sets, with no spatial or homotopical structure. However, a priori there is no reason this has to be the case.

One of the central insights of category theory and homotopy theory is that no class of mathematical objects should be considered without the corresponding notion of isomorphism or equivalence: we study groups up to isomorphism, spaces up to homeomorphism, categories up to equivalence, and so on. Thus, all mathematical collections naturally form groupoids when equipped with the relevant “notion of sameness”. The theory of all groups is much less tractable, and much less interesting, than the category of all groups; so even though the former is “simpler” in the sense of containing no nontrivial automorphisms, it is reasonable to regard the latter as being at least as fundamental.

One possible objection to treating spaces as fundamental is to ask how we should decide which rules our “spaces as fundamental” should satisfy. [Different mathematical fields] will have their own toposes and their own type theories.

[But] why must we insist on singling out some particular theory as “the” foundation of mathematics? The idea of a “foundation for mathematics” stems from the great discovery of 20th century logic that we can encode mathematics into various formal systems and study those systems mathematically. But in the 21st century, we are sufficiently familiar with this process that we no longer need to tie ourselves to only one such system. In ZFC orthodoxy there is an absolute notion of “set” out of which everything is constructed. Spaces exist, but they are second-class citizens, ultimately reducible to sets, and the basic axioms of set theory don’t apply to them. But from a pluralistic viewpoint, mathematics can be developed relative to any topos, obeying the same general rules of type theory. We have consistent rules for translating between toposes along functors, and there are some toposes in which mathematics looks a bit simpler. However, there is no justification for regarding any particular topos or type theory as the “one absolute universe of mathematics”. Just as modern physicists switch reference frames as needed, modern mathematicians should be free to switch foundational systems as appropriate. Set theory and 20th century logic were a crucial stepping-stone to bring us to a point where we can survey the multitude of universes of mathematics; but once there, we see that there is nothing special about the route we took.

Those sentences are taken from the conclusion of a recent arXiv paper by Michael Shulman on ‘Homotopy type theory: the logic of space‘, a long chapter written for a forthcoming book (I’ve not marked all the lacunae in this quotation which I’ve brutally cut by more than half). Unfortunately, despite Shulman’s expository gifts in some of his other exoteric papers, what comes before I find pretty impenetrable: but I’m sure that the problem is with me lacking enough background, not with Shulman’s ideas. So I’m still promising myself to try to get my head around what, in this vein, is happening in homotopy type theory, at least well enough to see what there this in the more philosophical claims made for it.

But that’s for after I get IFL2 sorted …