In what respect are univalent foundations "better" than set theory?

Question

It was an ambitious project of Vladimir Voevodsky's to provide new foundations for mathematics with univalent foundations (UF) to eventually replace set theory (ST).

Part of what makes ST so appealing is its incredible conciseness: the only undefined symbol it uses is the element membership $\in$. UF with its type theory and parts of higher category theory seems to be a vastly bigger body to build the foundation of mathematics. To draw from a (certainly very imperfect) analogy from programming: ST is like the compact C programming language [1], but UF seem more like the vast language of Java with all its object-oriented ballast [2].

Question. Why should mathematicians study UF, and in what respect could UF be superior to ST as a foundation of mathematics?

---

[1] One of my favorite quotes in "The C programming language":

"C is not a big language, and it is not well served by a big book". -- Brian Kernighan

[2] I never got the hang of object orientation, and whenever this subject comes up, I respond with this quote:

“The problem with object-oriented languages is they’ve got all this implicit environment that they carry around with them. You want a banana but what you get is a gorilla holding the banana and the entire jungle.” -- Joe Armstrong

Answer 1

I like your analogy with programming languages. If we think of ST as a low-level programming language and UF as a high-level one, then one advantage of UF is obvious: it is more convenient to write proofs (programs) in a high-level language. It is feasible to write proofs in UF, but it's virtually impossible to write down even statements of theorems in plain ST. This argument shows that UF is more convenient in practice than ST (well, I didn't give any proofs of this statement, but they can be found somewhere else, see this question and this list for example), but your question is about foundations and not about practice, so let me address this aspect.

Let me give two reasons why UF may be better as a foundation of mathematics than ST. The first reason is that all the constructions in homotopy type theory are stable under isomorphism, so if you prove a property of (let's say) a group, then this property is true for any isomorphic group. This is not true in ST and this problem is usually swept under the carpet. Another argument is that the category theory in UF is more well-behaved. For example, we have the concept of anafunctors in ST, but we don't need them in UF since they coincide with ordinary functors for univalent categories.

Finally, let's discuss the problem that UF is more complicated than ST. I claim that it's not actually true: ST isn't much smaller than UF. ZFC has (about) 10 axioms, but it is based on the formalism of first-order logic which has quite a few rules too. A types theory combines the rules of the logic and axioms of a set theory into one system (which, I think, is more elegant, but it's a matter of taste I guess). To prove that the number of constructions of a type theory is roughly the same as FOL+ZFC, let me just list some of them. On the left we have a type theoretic construction and on the right I write a FOL+ZFC construction which is analogous or similar (this correspondence is very informal and isn't precise).

• Sigma types / Existential quantifier, Axiom of union
• Pi types / Universal quantifier, Axiom of power set
• Sum types / Disjunctions, Axiom of pairing
• Identity types / Equality
• Natural numbers types / Axiom of infinity
• Universes / Large cardinals
• Univalence axiom (for propositions) / Axiom of extensionality

I could continue this list, but this relationship isn't precise, so let me stop here. You can see that some type theoretic constructions correspond to two different constructions on the FOL+ZFC side. This is because the logic and the set theory are fused together in TT, propositions are just a special kind of type. So one construction in TT may correspond to two constructions in FOL+ZFC. Thus the basic (homotopy) type theory has less constructions than FOL+ZFC. You can extends TT with other constructions such as (higher) inductive types, but you don't have to. The basic version of TT with the axiom of choice is roughly equivalent to ZFC (this statement can be made precise, but that's beside the point). So you get an equivalent theory with less constructions and (arguably) more elegant presentation. Moreover, you can get not only a set theory, but also a theory of homotopy types almost for free, you just need to add a very simple extension (universes + the univalence axiom).

Answer 2

This is a question that has been discussed a lot on the Foundations of Mathematics mailing list (unfortunately with more polemics than necessary IMO—though I confess that I may have been guilty of stoking the flames somewhat because I love to watch a good argument!).

My feeling is that to ask whether univalent foundations or set theory is the "better foundation for mathematics" is to start off on the wrong foot. Phrasing the question that way seems to take for granted that we know (1) what a "foundation for mathematics" is, (2) what makes a foundation good, and (3) that if we choose Foundation 1 instead of Foundation 2 then it will be because Foundation 1 is "better." I don't think that any of these should be taken for granted. There are multiple axes along which one may evaluate the quality of a proposed foundation for mathematics.

I think that it is better to start off by asking what UF is and what it is good for. Probably the most important point to recognize is that homotopy theory (or large chunks of it at least) turn out to be very naturally formalized in type theory, and much less naturally formalized in traditional set-theoretic foundations. Let me quote an FOM post by Urs Schreiber:

It had been mentioned here before that homotopy type theory offers some advantages for formal set-based mathematics, such as providing quotient types and isomorphism invariance. What seems not to have been mentioned much before here is that the key point of homotopy type theory however is that it goes way beyond this in that it provides a native (i.e. direct, synthetic, see below) formalization not just of constructive set theory, but of homotopy theory (aka algebraic topology). And the neat thing is: of homotopy theory in its modern and most powerful incarnation in the guise of infinity-toposes.

Just like plain dependent type theory is the internal language of locally cartesian closed categories, so homotopy type theory is the internal language of locally cartesian closed infinity-categories, and homotopy type theory with univalent type universes is the internal language of infinity-toposes. This means that homotopy type theory provides a "structural" foundation of the kind that William Lawvere had found in topos theory, but refined to homotopy theory in the refined guise of infinity-topos theory.

The fact that homotopy theory and type theory are so well-adapted to each other is a non-trivial insight. From a traditional set-theoretic point of view, homotopy theory at first glance requires slightly more than ZFC, because it invokes Grothendieck universes. However, it turns out that the core of the subject requires much less logical strength than that. Again let me quote someone, this time Neel Krishnaswami:

Voevodsky is coming to type theory from the point of view of a homotopy theorist. The traditional set-theoretic formulations of that subject make use of Grothendieck universes, and so go beyond ZFC. However, the big discovery of his univalent foundations project is that homotopy theory has a natural formalization in Martin-Lof type theory, which has the proof-theoretic strength of Kripke-Platek set theory (ie, vastly less than ZF). (IIRC, Anton Setzer has written a survey paper on this, "Proof Theory of Martin-Lof Type Theory: an Overview".)

Generally, it's no surprise when a theorem can be encoded in a weaker foundations, but the real shocker behind homotopy type theory is that a suitable type-theoretic view seemingly requires fewer encoding tricks than the traditional view. The apparent need for large constructions vanishes because the type structure of type theory prevents you from performing constructions which are okay on points but which fail to respect geometrical invariants like continuity. As a result, you can now talk about plain old functions instead of natural transformations on sheaf categories or whatever.

One practical consequence of this is that large chunks of homotopy theory can be (and have been) readily formalized using a proof assistant that is designed with UF in mind. Indeed it is impressive how much cutting-edge homotopy theory has been actually mechanically formalized; I'm not sure that any other subfield of mathematics can compete in this regard.

Now, one can counter (and some have countered) that formalizing the Blake-Massey theorem—or other important theorems in homotopy type theory that have been touted as successes for UF-based proof assistants—can be done with only a modest amount of additional effort using other type-theoretic proof assistants or even set-theoretic proof assistants. One can also counter that the theorem that is being proved in UF is not literally the same theorem that we would get by expanding all the definitions in a traditional set-theoretic manner, and so it's "cheating" to gloss over the work needed to show that the type-theoretic formulation and the set-theoretic formulation are essentially equivalent. These objections are technically correct, but I think that they obscure the important point that homotopy theory and UF really are an extremely natural fit.

Things get more interesting when we ask whether UF is well-suited to other areas of mathematics besides homotopy theory. In principle, UF is powerful and flexible enough to formalize most if not all of mathematics. The question is, why would you want to? There are a couple of possible reasons.

1. It could be that formalizing mathematics with a UF-based proof assistant is a lot easier and more natural than in any other proof assistant. Outside of homotopy theory, I think that the jury is still out on this one. Type-theoretic proof assistants such as Coq, HOL Light, and Isabelle do seem to have gained the upper hand over Mizar (probably the most significant proof assistant based on set theory), though it's unclear to me whether this is due to intrinsic advantages of type theory over set theory. But would a UF-based proof assistant have made it significantly easier to formalize the four-color theorem or Feit–Thompson? As I said, I think it's too early to make a definitive judgment.

2. It could be that UF provides a better conceptual foundation for all of mathematics than set theory does. The jury may still be out on this one too, but in my opinion it is doubtful that UF will ever completely supplant set theory in this regard. In a sense, the question is something of an academic one. Arguably the most important question in the foundations of mathematics is whether all of mathematics can be put on a common foundation in a simple and rigorous manner, and that question has already been answered affirmatively, by set theory. Once the job has been done, it is much less difficult to see how to use some other approach to unify all of mathematics, because we can always piggy-back on set theory. One can make aesthetic arguments for some other foundation, but it will be hard to escape the feeling that the choice of foundation is a matter of personal taste.

To summarize: UF does seem to be the "right" foundation for homotopy theory, although to appreciate this fact fully, you might need to learn quite a bit of homotopy theory. Whether UF is the "right" foundation for a broader swath of mathematics than that—well, my personal feeling is that we should adopt a "wait-and-see" approach and keep an open mind.

Answer 3

The two main things I find compelling about type theory as a foundation are:

1. A more direct way to deal with $\infty$-groupoids.
2. A closer match to how mathematicians actually talk about mathematics.

Timothy Chow's answer touches on point 1, so let me just add that personally I had a lot of trouble understanding and dealing with set theoretic definitions of $\infty$-groupoids, and find the HoTT definition natural and easy to work with.

The second one I think is pretty important. If you ask an actual mathematician whether 5 is an element of 7 or what the intersection of the Monster group and the real numbers is, they'll tell you "that question doesn't make sense!" But in set theoretic foundations those kinds of questions do make sense and have answers! In type theory the answer is "that doesn't type check," which is the slightly formal version of "that doesn't even make sense."

This sort of "type checking" is really important practically! It's like dimensional analysis and often quickly tells you when a formula is wrong or gives you a good guess as to what could possibly be true.

Even for really simple things like the set theoretic definitions of particular natural numbers, of ordered pairs, and of functions, the answer that set theory gives is not at all like the typical mathematicians intuition. But the type theoretic definitions do closely match my intuition. An ordered pair is a new type of thing and you're allowed to make an ordered pair by telling me the first entry and the second entry. A function is a new type of thing and if you tell me something in the source it tells you something in the target.

Answer 4

I would not say that Homotopy Type Theory is a replacement for set theory or make any kind of value judgment about it. The reason I think it's interesting and potentially useful comes from Freyd's proof that the category of weak homotopy types is not equivalent to any concrete category. In HoTT, the notion of 'set' is replaced with a primitive notion of homotopy type, so the category of homotopy types in HoTT replaces the category of sets as primitive. This means that within the rules of HoTT, we can do direct computations on with homotopy types.

I was at a conference recently, and André Joyal explained how a proof of a generalized version of the Blakers-Massey theorem came directly from translating the HoTT proof, and how the intuition behind it was very strange if you looked at things from the classical point of view, but apparently in HoTT, it's a very natural and clean proof.

At the conference, a number of people have been working on methods to develop a categorical semantics for HoTT (a lot of things involving polynomial functors), which should make HoTT more accessible to mathematicians who don't have the patience to work in type-theoretic semantics.

In particular, André Joyal has a new preprint kicking about that translates much of HoTT into more familiar structures for category theorists, which he calls clans and tribes. Steve Awodey also gave a talk describing similar structures, but I don't see a paper about it yet on the arXiv.

Answer 5

In my own idiosyncratic opinion, the central notion here is that of equivalence.

Traditionally, equivalence is a proposition: two things are either equivalent or they aren't, and there's no further structure to the notion. One of the most basic notions of classical logic is that of equality, which is such an equivalence relation.

However, it's become increasingly clear that equivalence is a more complex concept. In a great many examples, the relation of "is isomorphic to" is simply not that interesting: what you care about is the notion of isomorphism.

For example, the first isomorphism theorem of group theory is not "$G / \ker(\varphi)$ is isomorphic to $\operatorname{im}(\varphi)$"; it is "there is a map $G/\ker(\varphi) \to \operatorname{im}(\varphi)$ defined by $\overline{x} \to \varphi(x)$ and it is an isomorphism".

The basic insight of UF is to take this richer notion of equivalence as the primitive notion, rather than that of equality.

Answer 6

Let me try to answer the question in an oblique way. I should apologise in advance for the poor quality scan below. I have been thinking about the distinction it illustrates quite a bit lately and this seemed like a good opportunity to put forth some of those thoughts.

To me the foundations of mathematics can be defined as that which you need in order to implement some system of mathematics. This implementation can be conceptual or actual. You might want to develop your lines of mathematical thought more systematically in order to understand what you are doing as a mathematician at some deeper conceptual level; or you might want (as I do) to implement an actual real world system that would help you and others to do mathematics on a computer and gain some confidence that what you are doing is correct according to some well defined criteria.

Returning to the first sentence of the last paragraph for a moment, it seems to me that, crucially, the foundations of mathematics cannot be mathematics itself. This is probably a contentious opinion but I will try to justify it, and find a way through it, later on.

Now suppose that you want to implement some system of mathematics. Very broadly speaking you need three things:

1. Some sort of type system. This gives you the concept of types, obviously, but also variables, constructors, etc and therefore terms, expressions, etc. Syntax, basically, and the rules that go with it. It might also give you the concept of equality. It used to be the case that second-order logic was employed to give you much of this. It is often stated that you can implement the axioms of Peano arithmetic in second-order logic, for example. These days, however, second-order logic appears to have been largely superseded by type theory. You can think of the type theory I refer to here as the LaTeX explanation of the type system, if that doesn't sound too glib.

2. Some sort of proof system. This gives you concepts of propositions as atomic things that can be treated as building blocks stuck together with inference rules. It gives you concepts of contexts, assumptions, suppositions and derivations. And it gives you the concept of something being true, or just holding. You actually don't need concepts of truth and falsity, funnily enough. Essentially some statement holds if there is a proof of it. So the system is intuitionistic in this sense. Note that I'm saying the it is the proof system itself that bears the stamp of being intuitionistic and not some logic or other. Also again I'm calling the proof theory the theoretical distillation of the proof system.

3. A vernacular. This gives you concepts of therems, axioms, etc and most importantly, proofs. It also provides the means of communication. Personally I'm always careful to avoid the word 'language' and prefer 'vernacular' even though it's a bit flowery. I won't try to justify my motives here.

Of course, you won't get agreement from anyone about what exactly constitutes these three parts or how they hang together. No doubt many would disagree wholly with all of this. I can only say that from personal experience this is what you need if you want to do some mathematics from the ground up. And I call all of this foundations of mathematics for that reason.

At this point I can safely dismiss set theory as foundations of mathematics entirely because it is itself mathematics and plays no part in the above.

Now I can come to the schematic below (apologies again for the poor quality):

I've seen it asserted many times that mathematics is circular. Here is an example and there are many others:

Does mathematics become circular at the bottom? What is at the bottom of mathematics?

Why the confusion and why is there seemingly no clarity on this? In my opinion the reason is that the distinction between foundational concepts and their mathematical counterparts seems to be hardly ever made. Let me give an example of what I mean by that in order to clarify.

In foundations you have the concept of a context. A context is a bunch of statements that have been proven to hold by way of a theorem or have been given as holding by way of an axiom. These statements are uniquely labelled so that they can be referenced. Theorems themselves have local contexts. Statements that hold can be assumed in, or imported into shall we say, a theorem, for use therein. You can, for example, make use of the fact that $\sqrt 2$ is irrational if you have proved it somewhere already in a theorem and labelled that theorem uniquely.

However, if you show a mathematician a context they will say something along the lines of ''sure, it's a set of ordered pairs'' or ''it's a mapping'' and won't be persuaded otherwise. They see a context as a mathematical object. A set, in fact. No surprises there!

But it isn't. It's a context, just a context. It's a foundational concept, not a mathematical one. Notice how I used to sloppy language to define it. I used the phrase ''bunch of''. This was quite deliberate. I didn't want to fall into mathematical language, but in fact often it's almost impossible not to when considering many foundational concepts. This begs the question:

Is it a legitimate pursuit to treat foundational concepts as mathematical ones?

I have two answers to what I regard as the most important of all questions (!):

1. I don't know. I'm not smart enough to work it out.
2. The question is moot. Because mathematicians have been and always will do it anyway.

Which brings me on to the whole Univalence thing. I dismiss this as foundations also. Why? Not because it appears to be really too clever and complicated for my liking. It is, but I know that's mostly my problem. I dismiss it because I think they are failing to make the above distinction.

It seems to me that those involved liken mathematics to some kind of computer language and that the aim, like most computer languages, is to get it to ''compile itself''. Nerds love this kind of thing but I think in mathematics it is misguided, although I'm lost for a way to express exactly why.

What I will write though, at the risk of repetition, is that it is important that anyone engaged in the study of foundations recognises the distinction between that and the mathematics it results in. And that they should at least try to justify, and indeed should consider seriously, the treatment of former in terms of the latter.

Answer 7

If you are fully satisfied with classical logic and set theory as foundation of mathematics, no chance to convince you in a few words that univalent foundations can be "better". If you are not fully satisfied, you should take time to understand the concepts behind univalent foundations to see if it solves your frustrations.

Mathematicians interested in foundation of mathematics should take time to understand how logic and structures are handled in HoTT (Constructivity, propositions as types, proofs as programs, equality as identity types), and why this can be seen as a generalization of classical logic and standard set theoric constructions.

A theory that generalizes classical logic and set theoric constructions is likely to be a better foundations for mathematics, at least from the "philosophical" point of view, if not from a practical one.