It was an ambitious project of [Vladimir Voevodsky](https://en.wikipedia.org/wiki/Vladimir_Voevodsky)'s to provide new foundations for mathematics with [univalent foundations (UF)](https://en.wikipedia.org/wiki/Univalent_foundations) 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](https://en.wikipedia.org/wiki/C_(programming_language)) (about which Brian Kernighan [wrote](https://en.wikipedia.org/wiki/The_C_Programming_Language): "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](https://en.wikipedia.org/wiki/Java_(programming_language)) 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?



In what respect are univalent foundations "better" than set theory?
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](https://mathoverflow.net/questions/224297/practical-advantages-of-univalent-foundations) and [this list](https://ncatlab.org/nlab/show/homotopy+type+theory#Advantages) 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](https://ncatlab.org/nlab/show/anafunctor) 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).


