# In what respect are univalent foundations “better” than set theory?

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 C programming language (about which Brian Kernighan wrote: "C is not a big language, and it is not well served by a big book"), but UF seem more like the vast language of Java with all its object-oriented ballast.

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

• I don’t think will they eventually replace set theory as a foundation of mathematics is an appropriate question for this site. It would be more suitable at seer.stackexchange.com . – Emil Jeřábek Nov 24 '17 at 15:19
• Voevodsky's motivation was to build a proof assistant for doing homotopy theory (it is actually what he wrote in one of his paper). His motivation comes from some papers he published in the beginning of his career about the Homotopy Hypothesis and weak $\omega$-groupoids and which turned out to be wrong. His notion of $\omega$-groupoid is strictly associative with weakly invertible elements and it was proved later that a strictly associative law cannot lead to a model of all homotopy types. Troubles begin in dimension $3$. – Philippe Gaucher Nov 24 '17 at 15:45
• Another comment: I've heard a lot about univalent foundations and HoTT from people who like it very much. I'd be curious to have the point of view of people who studied it at some length but did not find it compelling. (Perhaps set theorists?) Also, I'd like to know what the proof-theoretical status of univalent foundations is (as in "it proves the same theorems of arithmetic as this-or-that version of set theory"); maybe this should be another question (but I'm not even sure it's meaningful). – Gro-Tsen Nov 24 '17 at 20:31
• In the programming analogy Set Theory isn't C, it's Assembler --- an architecture-dependent description that is sufficient for any problem but isn't really good for anything complicated, since it's boggled in arbitrary encodings and doesn't naturally allow us to use any kind of abstractions. UF isn't like Java, it's like Haskell in a very specific way. Different type theories could indeed give something like Java or C++. – Anton Fetisov Nov 25 '17 at 0:00
• Minimalism isn't a strictly good thing. To push the programming language analogy, see Turing tarpit. – user13113 Nov 25 '17 at 1:53

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).

• ZFC actually has infinitely many axioms, and one can prove that you cannot find an equivalent finite set of axioms. This doesn't change much of what you said, but it's just a correction to "ZFC has (about) 10 axioms" – Maxime Ramzi Nov 25 '17 at 8:43
• @Max Nice catch, but the "infinitely many" are all dictated by the single axiom schemata of set-building axioms, so this laziness is not too harmful here I think. – Alec Rhea Nov 25 '17 at 16:36
• By comparing the size of encodings into Automath, Freek Wiedijk gives quantitative estimates of how much more complex MLTT is than ZFC (including the cost of formalizing FOL). There's roughly a factor of two difference across a few metrics (e.g. number of primitive concepts, compressed size of the encoding). Of course, the "cognitive load" is unable to be quantified. It's not completely surprising as MLTT is constructive which means some symmetry is lost requiring additional primitives. Also, MLTT is more usable out-of-the-gate than ZFC. – Derek Elkins left SE Nov 26 '17 at 2:21
• I find the argument that "in set theory we can prove different statements about isomorphic group" is sort of like saying "hey, how about a bleach enema for cleaning your colon?". Yes, technically you're right, there is a trivial group where $\omega$ is the only element, and there is another where $\mathcal P(\omega)$ is the only element, and these are different. But this ignores context entirely, since you're not proving something about the group, you prove it about the underlying set. When you say "prove something about the group", [...] – Asaf Karagila Nov 27 '17 at 10:02
• [...] it implies (to me anyway) that you're talking about a statement in the language of groups, using some first/second/third/etc. order logic. But these various logics do not have access to the actual underlying set. So this is not really a statement about the group anymore. – Asaf Karagila Nov 27 '17 at 10:03

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.

• What is your take on Joyal's efforts to encode HoTT in category theory to make it more accessible to those of us less interested in writing formally verified proofs in a proof assistant? – Harry Gindi Nov 25 '17 at 1:54
• @HarryGindi : I'm afraid I don't know enough about that to comment intelligently. – Timothy Chow Nov 25 '17 at 1:56
• I linked the preprint in my answer. It's brand new, put up on Oct 30th. I'm interested to hear comments on it from someone who knows a lot about HoTT =] – Harry Gindi Nov 25 '17 at 1:59

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.

• Agreed; I wrote a blog post describing my sense of the informal type system that mathematicians are already using (but usually not making explicit) here: qchu.wordpress.com/2013/05/28/the-type-system-of-mathematics A related thing that's strange about ZFC is that it defines sets to be, essentially, a type of tree, but for the purpose of actually doing mathematics we ignore almost all of the tree structure when we consider sets up to isomorphism. – Qiaochu Yuan Nov 25 '17 at 19:34
• I hate that sort of argument against set theoretic foundation. I find it silly. If you also tell your run of the mill analyst that $0$ of $\Bbb R$ and $0$ of $\Bbb C$ and $0$ of $\Bbb N$ and $0$ of $\Bbb Z$ and $0$ of $\Bbb Q$ are all different mathematical objects, you are probably going to get the same reaction as you would when you ask what is the set $\sin\cap\cos$. – Asaf Karagila Nov 25 '17 at 20:01
• Though I also think that's very special to exactly the situation of "traditional numbers" and not to anything else in mathematics, and so one could argue that that intuition is problematic. I mean are the 0 in $\mathbb{Z}$ and $\mathbb{Z}/n\mathbb{Z}$ different mathematical objects? Certainly the $0$ in $\mathbb{C}$ and the $0$ in $\mathbb{Z}/n\mathbb{Z}$ are different! – Noah Snyder Nov 25 '17 at 20:13
• Also when we teach we acknowledge that this is a spot where we're doing something confusing. That is the first few pages about groups will be careful to distinguish between units or multiplication in different groups using notation like $\cdot_G$ and $e_G$, but then we drop that quickly afterwards. So it's somewhere that we're aware that a formal version should be more careful than the informal. Also, it's a fair and often good question in class to ask "Sorry, where is that multiplication taking place?" but a bad and troll-y question to ask "How many elements does that multiplication have." – Noah Snyder Nov 25 '17 at 20:24
• Of course, many mathematicians will also say that the question "is $\pi$ surjective" does not make such sense, and that the possibly clarifying question "do you mean the $\pi$ in $\{\pi\}$ or the $\pi$ in $\mathbb{R}$?" also does not make sense. (If this doesn't make sense: in systems where "elements" of a set are actually functions into the set, the question whether an element is surjective is very well formed, just as questions about $\pi \cap \sin$ are well formed in set theory.) – Carl Mummert Nov 27 '17 at 1:53

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.

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.

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.

• Homotopy type theory is a type theory, indeed most of it is Martin-Löf Type Theory that's existed for decades and was not at all motivated homotopy theoretic concerns. Type theory in general and the way it's typically presented seems to exactly the sort thing you're talking about in the first part of your answer, so I find the few last paragraphs confusing. The homotopy theory is motivating the definition of HoTT, not providing it, and my impression is that most people working on it understand that (but maybe that's just the parts I focus which are the more type theoretic side). – Derek Elkins left SE Nov 26 '17 at 4:57
• I think this is a superficial argument. After reading your first few paragraphs, I'm led to conclude that there are at least as many "foundations" as there are mathematicians. With this point of view there is little value in discussing foundations, at least not as a proper mathematical subject. That said, I think your last few questions focus on the disconnect between your argument and what the subject of foundations of mathematics is really about. [...] – François G. Dorais Nov 26 '17 at 6:55
• [...] Ponder this alternate point of view regarding your last question: considering that every mathematical subject is mathematics, what is the mathematical subject of foundations of mathematics? Okay, this is an awkwardly phrased question: the setup is tautological and the question itself is perhaps meaningless... Nevertheless, try to think of foundations of mathematics as a mathematical subject... Once you're there, consider this further scenario: what if, during that process, you discover something which is mathematically interesting? Perhaps this is what foundations is all about... – François G. Dorais Nov 26 '17 at 7:01
• @DerekElkins Hi. I think your usage of 'motivating' here is a good one. You could say that studying a type theory with your mathematician's hat on, so to speak, provides insights into how that type theory should be formulated. So you could in this way justify the apparent circularity. The phrase 'informing' also comes to mind. It's a kind of positive feedback mechanism. This is just the kind of debate that I think is healthy. My point is that I don't really see it. – James Smith Nov 26 '17 at 11:05
• My argument is that if you're not willing to consider the possibility, then you can't get to the next step and see what foundations of mathematics is about. That is the disconnect. – François G. Dorais Nov 26 '17 at 23:03

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.

• This doesn't say anything specific about the value of univalent foundations; I think this should probably be a comment rather than an answer. – Noah Schweber Nov 24 '17 at 23:42