3 ms·
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 sa
by Chinjut 10y ago
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.
- AnimalMuppet 10y agoWell, 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. Weak omega groupoids? Not so much. [Edit: Excellent ELI5, though. Thanks.]
- Chinjut 10y agoSets 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.