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,

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,

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

(where `x ~~> y`

is notation for

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 *n* to a composite of *n* copies of `loop`

, and a negative integer *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

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 `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.