I’m still trying to decide how best to continue the forcing series, but while we wait, let’s talk about something that took me an embarrassingly long time to understand:
Why isn’t the circle contractible?
The topologists in the audience are probably thinking “because it has a hole, obviously!” but I’m talking about the circle and contractibility as defined by homotopy type theorists; when you approach these with intuition from logic rather than topology, seeing the “hole” is a little less obvious. To be fair, the type theoretic proof that the circle is not contractible is pretty straightforward, certainly easier than the traditional proof, but it feels a bit like sleight of hand, and I never found it very convincing by itself.
We’ll use some of the same bit of type theory as last time. As a refresher, we have terms which always come with types. We write to say “The term has type . We have lots of ways to form types and type will always come with ways of creating terms of type (called introduction rules) and ways of using terms of type (called elimination rules). Again, there are more rules, but we’re not too worried about them for now.
We’re still interested in dependent functions: Given a type and a family of types indexed by (say, for ), we have a type of dependent functions from to , which we write as . The type can also be viewed as the quantified formula , when represents a proposition. In fact, even when doesn’t represent a proposition, we can think of a dependent function as a witness that “for all , the type is inhabited”.
As Martín Escardó points out, “types are secretly topological spaces and functions are secretly continuous.” This means that we should actually be thinking of the “for all” in the above as a slightly stronger statement: we have a way to continuously exhibit inhabitants of each .
As discussed last time, we have a type representing equality: given two terms of the same type, say , there is a type (called the identity type), or more clearly . There are two basic ways to think of this type
- Logically: As the proposition that is equal to , in which case a term is a witness that is equal to .
- Topologically: This type is the space of paths from the point to the point , in which case a term is a path in from to .
For now at least, we’ll mostly be using the second interpretation; after all, we’re talking about a homotopy-theoretic property today. The one last point about identity types is that given a term , we have path . The term is called the reflexivity term or the constant path.
The topological intuition for identity types immediately motivates a definition for contractible: A type is contractible when it has a “center of contraction”– a point such that is inhabited. This seems to be saying “there is a point such that for all there is a path –that is, path-connectedness.
The astute reader will recall that just a few paragraphs ago, I said that definitions must be continuous, so this reading is misleading: a better reading is “for each we have a path which varies continuously with “, which is actually a way to read the classical definition of contractible.
Contractible types may seem somewhat familiar from the last post: in fact, contractible types are propositions, and propositions are either contractible (“one inhabitant up to homotopy”) or empty. (Edit: As Andrej points out below, this is not exactly true, but its double negation is: no proposition is neither contractible nor empty.) Contractible types have a few nice properties, 2 in particular:
- Every contractible type is equivalent to the unit type 1 (which has a single constructor *).
- For any two contractible types, and , there is a unique function (up to homotopy) (the one which takes the center of to the center of ). When , then this is the identity function.
The circle and transporting along paths
It took me a long time to convince myself that really represented some sort of continuous deformation; I never really believed all that stuff about types secretly being topological space and functions secretly being continuous. This meant I really saw the definition of contractible as “path-connected”
The prototypical example of a path-connected, non-contractible space is the circle, , so to see why my intuition was wrong, we may as well start with the circle. There are a lot of homotopy-equivalent ways to define the circle, but the central fact is that the circle is a loop. A loop is just a path, from some base point to itself, so we need a point which we may as well call
base. Then the circle is generated by:
- A term and
- A path
The meaning of “generated by” in the last sentence is captured by the following rule:
(Induction Principle for ) Let be a family of types indexed by , and suppose we have a term and a path , lying over
loop. Then we have a dependent function such that and .
To make sense of this, we need to know what it means to apply a function to a path, and what it means for a path to “lie over” another one. In explaining how to apply a function to a path, we end up answering what it means for a path to lie over another.
The application of a function to a path: If , it seems obvious that for any function we should always have ; in type theory, this means we should have a function (“ap” is short for application”). For a non-dependent function, this is indeed the case, and by abuse of notation, we we write instead of .
For a dependent function , it gets a little trickier: since the target type of a dependent function depends on its input, even if , it’s not immediately clear that and , even have the same type. If they don’t have the same type, they cannot be compared, so we need to do more work.
Homotopically, a type family corresponds to fibration (with being the fiber over ), and a dependent function is a section. That is, we have some “total space” (which type theorists write ), with subspaces resting above each , and a dependent function picks a point in for each .
Now, (still speaking homotopically) if we fix some point , a path lifts to a path , for some (notice the type) in this total space. We can then turn into a function by sending to . On the other hand, if we take a section of the fibration, the path gives rise to a path this path lies over in the sense that it projects from the total space down to . Any path over factors through : there is a path in , from to such that the composition is ; or, in terms of our function , we have a path .
Back to type theory: we can simulate this whole argument in homotopy theory, but the order we do things in changes: The big difference is that in type theory, we “stay within the fibers”; as a result, we forget about and the path I called above. Instead, we work with the map (which is easier to define in type theory than the lifting), and we use the map I called instead of the one I called ; then becomes the path “lying over” . Explicitly
When and for some dependent function , we say that lies over .
All of this is to say, in the case of a dependent function , the theorem stating that “if , then “, becomes
For any dependent function and any path , we have a path .
In other words, while we don’t necessarily have an equality (since this isn’t guaranteed to make sense), if we transport f(x) along , we do have an equality.
As with , we will typically abuse notation and use instead of .
Non-contractibility of the circle
Back to the induction principle for the circle: If we have a -index family , and we find some and some lying over , then we can create a map such that and . This really is an induction principle: we have two generators, and , and by determining what happens with them, we know what happens with the whole structure. The requirement that lies over is so that has the correct type, namely .
The requirement that lies over is also why we can’t contract the circle: To say the circle is contractible, we want a term . (We could, of course, use some other point… but where would we get this other point from?) This is a perfect place to apply induction: we need to send the basepoint to some path . We have two “obvious” choices: the reflexivity term, or the loop. Let’s just try . Then we need to send to some path .
This is a bit of an awkward place to be: it’s not clear (and intuitively fishy) that transporting along the loop brings you to where you started–after all, that’s how you prove that . And of course, it’s not true. We could try to send to , but we’ll run into similar problems.
So, we can’t contract the circle (or at least, not in an obvious way), which is probably a good thing.
Pointwise paths, truncation
On the other hand, I’ve said a few times that can be interpreted to mean “for all”, and we should have “for all points in the circle, there is a path to the basepoint.” It wouldn’t be much of a circle otherwise. So how do we get this theorem without contracting the circle?
The answer is to use truncation. The propositional truncation or -1-truncation (“minus 1 truncation”) of a type is essentially the “quotient” of by the total relation: for each we have , and we have paths . Intuitively, just connect every single point to every other point “continuously”. This turns out to be a proposition (either contractible or empty), and is inhabited iff is.
What if instead of we tried ? Again, we proceed by induction, and we send to the reflexivity term –actually, this doesn’t have the correct type. We need to take –the “truncated version”. Now look at our function . Remember earlier I said there’s only one function (up to homotopy) between contractible types? Well, this one function must be the identity. So then we know that . And then we can apply the induction principle to get some term of type .
And the Axiom of Choice
The difference between and is subtle: the first says that each type is inhabited, but we (may) have no algorithm for finding such an inhabitant; the second says that we can algorithmically determine these elements. It’s pretty strange that a constructive theory allows us to make non-constructive statements!
But a question arises: when can we say that implies ?
One of my favorite ways of expressing the axiom of choice is: “The product of a non-empty family of non-empty sets is non-empty”. Turned into type theory “a non-empty set” becomes a set with an inhabitant, but we should forget about “constructive content” to get “ is non-empty” as . We can then translate (this version of) AC into type theory as:
(Axiom of Choice) For any set and family indexed by , we have .
In the statement of AC and in the preceding paragraph I intentionally used the word “set” where you probably expected the word “type”. That’s because AC (AC for all types) is inconsistent with univalence (after all, the circle is a counterexample). However, it’s consistent to assume the axiom of choice for sets, which we will leave for another day.