Constructive logic is logic without the Law of Excluded Middle. It is the part of mathematics that is actually relevant to computing. HoTT serves as a good fou

Constructive logic is logic without the Law of Excluded Middle. It is the part of mathematics that is actually relevant to computing. HoTT serves as a good foundation for constructive logic; perhaps better than any other. Set theory (like ZFC) makes doing constructive logic very awkward, as the very idea of an infinite set (which can be union'd and intersected with any other infinite set) is unnatural in such a logic (but can be made to work if you accept some pain). Martin-Lof Type Theory isn't "good enough", because it handles equality quite poorly, which is fundamental to logic. For instance, how would you state the Axiom Of Unique Choice in Martin-Lof Type Theory? The idea behind HoTT (over Martin-Lof TT) is that path-connectedness in a topological space is somehow more fundamental than equality. Equality is recovered when that space becomes discrete. Everything that's possible in set theoretic foundations is possible in HoTT, because a set is just a discrete topological space. Equivalence relations are constructed by simply building bridges between points, and then contracting connected components down to points. The idea behind Martin-Lof TT is that there is a rough duality between how you prove things and how you program things. Propositions correspond to types in MLTT, and proofs correspond to programs. In MLTT, this is taken to be an isomorphism between proofs->programs and propositions->types. In HoTT, this is usually not taken to be an isomorphism, as propositions are instead understood as only some of the types (the subsingletons). In MLTT, the whole point of constructive logic becomes clear. The proposition "There are infinitely many prime numbers" is a type (like in some programming languages) whose elements are programs which take integers as input and produce larger primes as output. If you look at the standard proof of "There are infinitely many prime numbers", you'll see that it determines an algorithm. This is not the best example, as the resulting algorithm is rather naive, but there are plenty of better examples. > It is sometimes quite useful in practice to recognize that two isomorphic objects are not literally the same. So I am skeptical of any approach that wants to blur those distinctions. It's called inverting a surjective function. You can do that in HoTT, or any foundation. In fact, this remark shows you're dangerously over-opinionated. > Also, more to the point: ZFC does everything we need a foundation to do extremely well, except serve as a basis for practical formalization of proofs. What does ZFC really do? The axioms are pretty obtuse, abstract, divorced from mathematical practice (who the hell needs to know that an integer is an infinite set), infinitary and non-constructive and hostile to computers.