A formal proof that π₁(S¹)=Z

The idea of higher inductive types, as described here and here, purports (among other things) to give us objects in type theory which represent familiar homotopy types from topology. Perhaps the simplest nontrivial such type is the circle, $S^1$ , which as a higher inductive type is claimed to be inductively generated by a point and a loop:

Inductive (circle : Type) :=
  | base : circle
  | loop : base ~~> base.

We can “implement” this type in Coq or Agda by asserting the type, its constructors, elimination rule, and computation rules as axioms. Peter’s post talks about deducing what the elimination rule should be.

If this is to really be a circle, we should be able to prove some familiar homotopy-theoretic facts about it. However, we will need some other new axiom to make the theory nontrivially homotopical, since if UIP holds then the circle is equivalent to the unit type (and in fact the converse is also true). The obvious choice for such an axiom is univalence, but is univalence sufficient to ensure that the inductively defined circle behaves like a circle? I don’t find this a priori obvious, but this post presents some evidence in that direction. Namely, assuming the univalence axiom, we can prove (and formalize in Coq) that the loop space of the circle, $\Omega S^1$ , is equivalent to the integers $\mathbb{Z}$ :

Theorem int_equiv_loopcirc : equiv int (base ~~> base).

(where x ~~> y is notation for $\mathrm{Paths}(x,y) = \mathrm{Id}(x,y)$ ). Since the integers are a set, this should imply that $\pi_1(S^1) = \mathbb{Z}$ as well, modulo a suitable definition of $\pi_1$ (for instance, as $\pi_0\Omega$ , for a suitable definition of $\pi_0$ ).

In order to prove this, first of all we need a definition of the integers. I used this one:

Inductive int : Type :=
| pos : nat -> int
| zero : int
| neg : nat -> int.

In other words, an integer is either one more than a natural number, or zero, or one less than minus a natural number. (Of course, the naturals are inductively generated by 0 and successor.) Some of the proofs could probably have been shortened a little by using “nonneg” and “neg”, or “pos” and “nonpos”, but I find the symmetrical version easier to not get confused about. A very important fact is that int, like nat, has “decidable paths”, and therefore is a set.

Now is easy to construct a map from the integers to $\Omega S^1$ : we send zero to the identity path, a positive integer n to a composite of n copies of loop, and a negative integer $-n$ to a composite of n copies of the opposite path !loop.

To get a map in the other direction requires the univalence axiom and a little cleverness. We define, by recursion, a function

succ : int -> int

which adds one to its argument, and prove that it is an equivalence. By univalence, it therefore induces a path int ~~> int in the universe Type. The elimination rule for the circle then gives us a map circle -> Type which sends loop to this endopath of int. Finally, given any path base ~~> base in the loop space of the circle, we can apply this function to it to obtain an endo-path of int, turn that path into an endo-equivalence, and then evaluate that equivalence at zero to get an integer. This gives us a map (base ~~> base) -> int, which ought to be an inverse of the map in the other direction defined above.

It’s not hard to prove by induction that the composite from int to (base ~~> base) and back to int is the identity. I believe we got about this far at Oberwolfach. But just staring at the definitions of these two maps, it seems not at all clear how to prove anything about the other composite. Instead, we have to take a different tack.

Open up any introductory algebraic topology textbook and find the proof that $\pi_1(S^1)=\mathbb{Z}$ . Odds are, it is proven by constructing the universal cover of $S^1$ as the “winding” map $\mathbb{R}\to S^1$ , and using the facts that $\mathbb{R}$ is contractible and that the fiber of the winding map is $\mathbb{Z}$ . We can mimic this in homotopy type theory, except that since our definition of $S^1$ is different, we need to construct the universal cover somewhat differently.

However, the universal cover is actually already staring us in the face! Remember that a fibration in homotopy type theory (such as a covering space) over a type A is equivalently a dependent type over A, which is to say a map $A\to \mathrm{Type}$ into the universe. And we have already constructed a map $S^1 \to \mathrm{Type}$ , above, which takes the basepoint to $\mathbb{Z}$ and the loop to succ; clearly this should be the universal cover when regarded as a fibration over circle.

With this idea in hand, the proof more or less writes itself, in the following steps:

Extend the above map int -> (base ~~> base) to a map of dependent types over circle between the putative universal cover and the path-space based at base. In other words, write a function of type
```
forall (x : circle), circle_cover x -> (base ~~> x)
```
Like any fiberwise map, this induces a map of total spaces
```
{ x : circle & circle_cover x } -> { x : circle & base ~~> x }
```
Prove that the total space { x : circle & circle_cover x } of the putative universal cover is contractible. I found it easiest to do this by using the fact that int is a set.
Since { x : circle & base ~~> x } is a based path space, it is also contractible. Therefore, the above map on total spaces is a function between two contractible spaces, and hence is an equivalence.
Prove that a fiberwise map which induces an equivalence of total spaces must already be an equivalence on each fiber. Vladimir proved this in his Coq file; I just copied his idea.
Specializing to the fiber over base, we find that the fiber of the universal cover, which is equivalent to int, is equivalent to (base ~~> base), which is the loop space of circle.

A Coq implementation of this proof is now available in the Coq/HIT directory of the HoTT repository. I decided to stick with propositional computation rules for circle, rather than using Dan Licata’s trick, for three reasons: (1) I’d already mostly completed the proof when I learned the trick; (2) Coq’s abstraction mechanism differs from Agda’s in such a way that the contradictions involved in the trick are not completely hidden, which makes me uneasy; and (3) since definitional equalities imply propositional ones, a proof using propositional rules says more than one using definitional rules. In particular, if there are any “coherence conditions” one might need to require of the propositional computation rules for HITs, they haven’t shown up yet.

2 Responses to A formal proof that π₁(S¹)=Z

Steve Awodey says:

30 April 2011 at 07:24

Very nice! I especially like the way univalence figures into building the universal cover. It is indeed evidence for univalence being a good “homotopy postulate”. We don’t really need to worry about excluding UIP, since it’s not implied by anything in the free theory anyway; but we do want to find new postulates that allow us to reason correctly in the homotopy interpretation. This is a lovely example of how univalence is one such.

I guess one thing this is also saying is that the inductive spec of the circle is correct in higher dimensions, too. It might have been the case that we get something with the right $\pi_1$ , but that it also has some non-trivial higher homotopies — say, because the type theory somehow fails to control the higher dimensions. However, your proof that the “space” $\Omega{S^1}$ is equivalent to the integers $\mathbb{Z}$ , and the fact that the latter is a set, shows that this is in fact not the case. So — assuming univalence — the inductive spec actually suffices to nail down the circle. Marvelous.

- Mike Shulman says:
  
  30 April 2011 at 12:57
  
  Thanks! I also like the role played by univalence, and how its “from the right” property matches perfectly with the “from the left” property of a higher inductive type to allow us to construct fibrations. All I meant about UIP is that the inductive spec of the circle doesn’t by itself rule out UIP, and if UIP holds, then $\pi_1(S^1)$ is certainly not going to be $\mathbb{Z}$ . As you say, what we need are new postulates that allow us to reason correctly in homotopy theory.