# Circles, Contractible Spaces, and the Axiom of Choice

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.

Type theory

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 $a:A$ to say “The term $a$ has type $A$. We have lots of ways to form types and type $A$ will always come with ways of creating terms of type $A$ (called introduction rules) and ways of using terms of type $A$ (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 $A$ and a family of types indexed by $A$ (say, $B(x)$ for $x:A$), we have a type of dependent functions from $A$ to $B$, which we write as $\displaystyle \prod_{x:A}B(x)$. The type $\displaystyle\prod_{x:A}B(x)$ can also be viewed as the quantified formula $\forall x\in A,\;B(x)$, when $B(x)$ represents a proposition. In fact, even when $B(x)$ doesn’t represent a proposition, we can think of a dependent function $d:\displaystyle \prod_{x:A}B(x)$ as a witness that “for all $x:A$, the type $B(x)$ 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 $B(x)$.

As discussed last time, we have a type representing equality: given two terms of the same type, say $x,y:A$, there is a type $x=y$ (called the identity type), or more clearly $x=_{A}y$. There are two basic ways to think of this type

• Logically: As the proposition that $x$ is equal to $y$, in which case a term $p:x=y$ is a witness that $x$ is equal to $y$.
• Topologically: This type is the space of paths from the point $x$ to the point $y$, in which case a term $p:x=y$ is a path in $A$ from $x$ to $y$.

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 $x:A$, we have path $r(x):x=x$. The term $r(x)$ is called the reflexivity term or the constant path.

Contractibility

The topological intuition for identity types immediately motivates a definition for contractible: A type $T$ is contractible when it has a “center of contraction”– a point $c:T$ such that $\prod_{x:T}(x=c)$ is inhabited. This seems to be saying “there is a point $c:T$ such that for all $x:T$ there is a path $x=c$–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 $x:T$ we have a path $p_x:x=c$ which varies continuously with $x$“, 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, $T$ and $S$, there is a unique function (up to homotopy) $f:T\rightarrow S$ (the one which takes the center of $T$ to the center of $S$). When $T\equiv S$, then this $f$ is the identity function.

The circle and transporting along paths

It took me a long time to convince myself that $\prod_{x:T}(x=c)$ 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, $\mathbb{S}^1$, 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 $\mathbb{S}$ is generated by:

• A term $\mathsf{base}:\mathbb{S}$ and
• A path $\mathsf{loop}:\mathsf{base}=_{\mathbb{S}}\mathsf{base}$

The meaning of “generated by” in the last sentence is captured by the following rule:

(Induction Principle for $\mathbb{S}$) Let $P(x)$ be a family of types indexed by $\mathbb{S}$, and suppose we have a term $b:P(\mathsf{base})$ and a path $l:b=_{P(\mathsf{base})}b$, lying over loop. Then we have a dependent function $f:\displaystyle \prod_{x:\mathbb{S}}P(x)$ such that $f(\mathsf{base})=b$ and $f(\mathsf{loop}) = l$.

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 $x=_Ay$, it seems obvious that for any function $f:A\rightarrow B$ we should always have $f(x)=_Bf(y)$; in type theory, this means we should have a function $\mathsf{ap}_f:(x=_Ay)\rightarrow (f(x)=_Af(y))$ (“ap” is short for application”). For a non-dependent function, this is indeed the case, and by abuse of notation, we we write $f(p)$ instead of $\mathsf{ap}_f(p)$.

For a dependent function $f:\prod_{x:A}B(x)$, it gets a little trickier: since the target type of a dependent function depends on its input, even if $x=y$, it’s not immediately clear that $f(x)$ and $f(y)$, 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 $B(x)$ being the fiber over $x$), and a dependent function is a section. That is, we have some “total space” (which type theorists write $\sum_{x:A}B(x)$), with subspaces $B(x)$ resting above each $x:A$, and a dependent function picks a point in $B(x)$ for each $x$.

Now, (still speaking homotopically) if we fix some point $u:B(x)$, a path $p:x=y$ lifts to a path $p_\sim:u=v_u$, for some $v_u:B(y)$ (notice the type) in this total space. We can then turn $p_\sim$ into a function $p_*:B(x)\rightarrow B(y)$ by sending $u$ to $v_u$. On the other hand, if we take a section $s$ of the fibration, the path $p$ gives rise to a path $s(p): s(x)=s(y)$ this path lies over $p$ in the sense that it projects from the total space down to $p$. Any path over $p$ factors through $p_\sim$: there is a path $q_p$ in $B(y)$, from $v_u$ to $s(y)$ such that the composition $p_\sim\cdot q_p$ is $s(p)$; or, in terms of our function $p_*$, we have a path $q_p: p_*(s(x)) = s(y)$.

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 $p_\sim$ and the path I called $s(p)$ above. Instead, we work with the map $p_* : B(x)\rightarrow B(y)$ (which is easier to define in type theory than the lifting), and we use the map I called $q_p$ instead of the one I called $s(p)$; then $q_p$ becomes the path “lying over” $p$. Explicitly

When $p:x=_Ay$ and $q:p_*(f(x))=_{B(y)}f(y)$ for some dependent function $f:\prod_{x:A}B(x)$, we say that $q$ lies over $p$.

All of this is to say, in the case of a dependent function $f:\prod_{x:A}B(x)$, the theorem stating that “if $x=y$, then $f(x)=f(y)$“, becomes

For any dependent function $f:\displaystyle\prod_{x:A}B(x)$ and any path $p:x=y$, we have a path $\mathsf{apd}_f(p):p_*(f(x))=f(y)$.

In other words, while we don’t necessarily have an equality $f(x)=f(y)$ (since this isn’t guaranteed to make sense), if we transport f(x) along $p$, we do have an equality.

As with $\mathsf{ap}$, we will typically abuse notation and use $f(p)$ instead of $\mathsf{apd}_f(p)$.

Non-contractibility of the circle

Back to the induction principle for the circle: If we have a $\mathbb{S}$-index family $P(x)$, and we find some $b:P(\mathsf{base})$ and some $l$ lying over $\mathsf{loop}$, then we can create a map $f:\prod_{x:\mathbb{S}}P(x)$ such that $f(\mathsf{base})\equiv b$ and $f(\mathsf{loop})\equiv l$. This really is an induction principle: we have two generators, $\mathsf{base}$ and $\mathsf{loop}$, and by determining what happens with them, we know what happens with the whole structure. The requirement that $l$ lies over $b$ is so that $\mathsf{apd}_f(\mathsf{loop})$ has the correct type, namely $\mathsf{loop}_*(f(\mathsf{base}))=f(\mathsf{base})$.

The requirement that $l$ lies over $b$ is also why we can’t contract the circle: To say the circle is contractible, we want a term $c:\prod_{x:\mathbb{S}}x=\mathsf{base}$. (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 $\mathsf{base}=\mathsf{base}$. We have two “obvious” choices: the reflexivity term, or the loop. Let’s just try $r(\mathsf{base})$. Then we need to send $\mathsf{loop}$ to some path $\mathsf{loop}_*(r(\mathsf{base}))=r(\mathsf{base})$.

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 $\pi_1(\mathbb{S}^1)=\mathbb{Z}$. And of course, it’s not true. We could try to send $\mathbf{base}$ to $\mathbf{loop}$, 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 $\prod$ 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”) $\|A\|$ of a type $A$ is essentially the “quotient” of $A$ by the total relation: for each $x:A$ we have $|x|:A$, and we have paths $\prod_{x,y:\|A\|}x=y$. 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 $A$ is.

What if instead of $\prod_{x:\mathbb{S}}x=\mathsf{base}$ we tried $\prod_{x:\mathbb{S}}\|x=\mathsf{base}\|$? Again, we proceed by induction, and we send $\mathsf{base}$ to the reflexivity term $r(\mathsf{base})$–actually, this doesn’t have the correct type. We need to take $|r(\mathsf{base})|$–the “truncated version”. Now look at our function $\mathsf{loop}_*:\|\mathsf{base}=\mathsf{base}\|\rightarrow\|\mathsf{base}=\mathsf{base}\|$. 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 $\mathsf{loop}_*(|r(\mathsf{base})|)=|r(\mathsf{base})|$. And then we can apply the induction principle to get some term of type $\prod_{x:\mathbb{S}}\|x=\mathsf{base}\|$.

And the Axiom of Choice

The difference between $\prod_{x:\mathbb{S}}\|x=\mathsf{base}\|$ and $\prod_{x:\mathbb{S}}x=\mathsf{base}$ is subtle: the first says that each type $x=\mathsf{base}$ 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 $\prod_{x:\mathbb{S}}x=\mathsf{base}$ implies $\prod_{x:\mathbb{S}}\|x=\mathsf{base}\|$?

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 “$A$ is non-empty” as $\|A\|$. We can then translate (this version of) AC into type theory as:

(Axiom of Choice) For any set $A$ and family $P(x)$ indexed by $A$, we have $\displaystyle{\left(\prod_{x:A}\|P(x)\|\right)}\rightarrow \|\displaystyle\prod_{x:A}P(x)\|$.

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$\mathstrut_\infty$ (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.