I don't understand HoTT. But every time I try to learn a bit about it, I go to the Wikipedia article (hey, everybody's got to start somewhere). And something always bugs me:
They're trying to build a foundation for all of mathematics. But their starting point requires weak omega groupoids. But weak omega groupoids are not exactly a fundamental object; you kind of need a foundation of something else before you ever get anywhere near weak omega groupoids. Their foundation, then, seems to me to be inevitably recursive.
Now, I get that the people involved in this are much smarter than me, and know far more mathematics. So, if you can, ELI5: Why isn't HoTT a recursive house of cards?
HoTT doesn't build on any notion of omega groupoids; at the lowest level it's a collection of typing and computation rules which one can apply successively to do proofs and constructions. The resulting constructions can be interpreted as talking about properties of spaces. The rules themselves are very stripped-down and abstract when viewed in a homotopical light, like "every path can be retracted to an endpoint" or "the interval has two points and a path between them". Originally the basic rule for reasoning about paths ("path induction") was intended to allow construction of equality proofs between elements of types. Later people discovered that equalities can be interpreted as paths in spaces (and equalities of equalities as homotopies and so on).
Remarkably, the four typing rules of equality suffice to generate all homotopical reasoning in classic HoTT. However, they aren't enough to prove univalence as a theorem, or at least no one knows how to do it. If we switch to cubical type theory, we get considerably more structure which allows us to prove univalence. But cubical type theory is also "synthetic" and builds up notions of spaces from ground-up.
Thanks to you (and Chinjut) for the replies. I don't know how to correlate your reply to Chinjut's, though (or vice versa). Could either of you take a stab at it? Are you saying the same thing in different ways? Or are you actually disagreeing?
So when you said, "at the lowest level it's a collection of typing and computation rules which one can apply successively to do proofs and constructions", That was what Chinjut meant by "Homotopy Type Theory axiomatizes weak omega groupoids; it gives you formal rules you can manipulate to reason about weak omega groupoids"? That is, those lowest-level rules don't assume weak omega groupoids; they turn out to define weak omega groupoids?
Homotopy Type Theory axiomatizes weak omega groupoids; it gives you formal rules you can manipulate to reason about weak omega groupoids. This is exactly the same way, say, ZFC axiomatizes sets of sets of sets… "You're allowed to shuffle symbols in these ways, and the results of doing so we shall call theorems".
There's not an intrinsic sense in which sets are "foundational objects" and groupoids aren't; yes, you can encode groupoids as set structures with certain properties, but in just the same way, you can encode sets as groupoid structures with certain properties. Or, for example, you can encode points and lines using coordinates and Dedekind cuts of rational numbers or what have you, but you can also do Euclidean geometry without first developing some theory of real number arithmetic in that fashion, just directly axiomatizing the relevant properties of points and lines.
Any formal system gives you some basic rules to work with; as long as you can communicate and understand the rules, you're good to go. You don't need any other prerequisites.
Well, it's pretty easy to say that math started with the counting numbers. It's not much more of a reach to say that when we were counting some collection of things, we were counting the elements of a set. So saying that sets are the foundation of mathematics is, historically, quite natural.
Sets of things are somewhat different from transfinitely iterated sets of sets of sets of sets, though… (I'll call these ZF-sets).
Discrete sets of atomic objects are in fact (special) weak omega-groupoids and aren't ZF-sets. (In a ZF-set, every element of a set is itself a set, which is not true of, say, {red, green, blue}, unless we impose some completely artificial and obfuscating coding). You could just as well say that when we were counting the elements of sets thousands of years ago, we were doing the first rung of building up weak omega-groupoids, rather than the first rung of building up ZF-sets.
The name "weak omega-groupoids" makes them sound more intimidating as a concept than they actually are. They're just certain kinds of shapes. A bunch of dots (like a discrete set) is a weak omega-groupoid. A circle is a weak omega-groupoid. Spheres and donuts are weak omega-groupoids.
That said, I don't assert that weak omega-groupoids are any more intrinsically a foundational concept than ZF-sets; rather, I just note that ZF-sets aren't particularly elementary, either.
They're trying to build a foundation for all of mathematics. But their starting point requires weak omega groupoids. But weak omega groupoids are not exactly a fundamental object; you kind of need a foundation of something else before you ever get anywhere near weak omega groupoids. Their foundation, then, seems to me to be inevitably recursive.
Now, I get that the people involved in this are much smarter than me, and know far more mathematics. So, if you can, ELI5: Why isn't HoTT a recursive house of cards?