Imagine you have different boxes for sorting things. In Homotopy Type Theory (HoTT), these boxes are called types, and the things you put inside them are called terms.
The most important idea in HoTT is about how we say two things are the same. Instead of just saying “this equals that,” we need to provide a reason or a path that proves they’re the same. This collection of reasons or paths is called an identity type.
The complexity of these “reasons for equality” determines what kind of collection you’re dealing with.
Level 0: Propositions (Simple Truths)
A proposition is the simplest kind of type. Think of it as a statement that is either true or false. If a statement is true, there’s only one, straightforward reason why it’s true.
For example, the statement “2+2=4” is a proposition. It’s true, and there aren’t different flavors of this truth—it just is. A type is a proposition if, for any two items in it, there’s at most one reason for them to be considered the same. It’s like a light switch: on or off. 💡
Level 1: Sets (Normal Collections)
A set is a collection of distinct items, like the numbers {1, 2, 3}. The reasons for equality are still simple propositions. For example, there’s a simple reason why 3 is the same as 3, but there’s no reason at all why 3 would be the same as 2.
Most of the math we learn in school (like arithmetic and basic algebra) deals with sets. You’re just checking if things are identical or not.
Level 2: Groupoids (Collections with Interesting Equalities)
This is where things get more interesting. 🧐 A groupoid is a type where the reasons for equality have their own structure. In other words, there can be multiple, distinct ways to prove two things are equivalent.
Imagine you have two pairs of socks.
-
Pair A is {Red Sock, Blue Sock}.
-
Pair B is {Green Sock, Yellow Sock}.
How can we say “Pair A is equivalent to Pair B” (since they’re both just pairs)? We can show this by matching them up in two different ways:
-
Reason 1: Match Red ↔ Green and Blue ↔ Yellow.
-
Reason 2: Match Red ↔ Yellow and Blue ↔ Green.
Since there are two different reasons (or paths) to explain their equivalence, the collection of “pairs of socks” isn’t a simple set. It’s a groupoid. The “identity type” connecting Pair A and Pair B contains two distinct proofs.
This allows us to make powerful statements, like saying the set of positive integers {1, 2, 3, ...} is equivalent to the set of negative integers {-1, -2, -3, ...} because we can create a clear mapping between them (n ↔ -n).
To Infinity and Beyond! (∞-Groupoids)
HoTT doesn’t stop there.
-
You can have 2-groupoids, where the reasons between the reasons also have their own structure.
-
You can have 3-groupoids, and so on.
This process can continue forever, leading to ∞-groupoids. These are types where the reasons for equality are just as rich and complex as the original items themselves. This is where the "homotopy" (which studies shapes) part of the name comes from: you can think of types as complex shapes and the identity paths as ways of moving around on their surfaces.