Here’s a more accessible version:
Homotopy Type Theory: A Theory of Objects and How They Can Be Equal
Homotopy type theory studies three main things: individual objects (which we call terms), collections of objects (called types), and the different ways objects can be considered equal to each other.
The key insight is that “equality” itself comes in different flavors depending on what kind of collection you’re working with.
Simple Collections (Propositions) Some collections are very simple. Either they contain nothing at all, or if they do contain objects, any two objects in the collection are equal in exactly one obvious way. Think of a collection like “all ways to prove 2+2=4” - there might be different proofs, but they’re all essentially the same thing. These simple collections are called propositions.
Everyday Collections (Sets) Most collections we think about daily work like traditional sets. Take a collection of people: either two people are the same person (equal) or they’re different people (not equal). There’s no middle ground or multiple ways for two people to be “the same.” These are called sets.
More Complex Collections (Groupoids) But some collections are more interesting. Imagine you have a collection containing “all possible ways to arrange two books on a shelf.” You might have:
- Arrangement 1: Book A on left, Book B on right
- Arrangement 2: Book C on left, Book D on right
Now, you could say these arrangements are “the same type of thing” in two different ways: you could match A with C and B with D, or you could match A with D and B with C. So there are multiple meaningful ways these arrangements can be considered equal. Collections like this are called groupoids.
Even More Complex Collections You can keep building up complexity. Just as groupoids have multiple ways for objects to be equal, you can have collections where those “ways of being equal” themselves have multiple ways of being equal. This creates 2-groupoids, then 3-groupoids, and so on.
At the top of this hierarchy are ∞-groupoids - collections where equality has infinitely rich structure, with layers upon layers of different ways things can be considered the same.
Why This Matters This framework gives us a precise way to talk about how different mathematical objects relate to each other, capturing not just whether things are equal, but the rich structure of how they can be equal. It’s particularly useful for understanding spaces, shapes, and transformations in mathematics.