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, , 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, , is equivalent to the integers :

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

(where `x ~~> y`

is notation for ). Since the integers are a set, this should imply that as well, modulo a suitable definition of (for instance, as , for a suitable definition of ).

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 : we send zero to the identity path, a positive integer *n* to a composite of *n* copies of `loop`

, and a negative integer 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 . Odds are, it is proven by constructing the universal cover of as the “winding” map , and using the facts that is contractible and that the fiber of the winding map is . We can mimic this in homotopy type theory, except that since our definition of 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 into the universe. And we have already constructed a map , above, which takes the basepoint to 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 typeforall (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.

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 , 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” is equivalent to the integers , 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.

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 outUIP, and if UIP holds, then is certainlynotgoing to be . As you say, what we need are new postulates that allow us to reason correctly in homotopy theory.