(This was written in inadvertent parallel with Mike’s latest post at the Café, so there’s a little overlap — Mike’s discusses the homotopy-theoretic aspects more, this post the type-theoretic nitty-gritty.)

Higher inductive types have been mentioned now in several other posts, so it’s probably time to bring the full troupe out into the sunshine and show them off a bit.

If we’re aiming to do homotopy theory axiomatically within type theory — if our types are homotopy types — then in particular, we should hope to have types around representing the most fundamental spaces of topology: the circle, the interval, the 2-sphere… So, how should we construct these types?

Well, most types in dependent type theory (in CIC/Coq, all apart from function spaces) are constructed as inductive types, or the slightly more general inductive families. In Coq syntax, for instance, one defines the natural numbers as the type freely generated by an element O and an endomorphism suc:

Inductive (Nat : type) :=
  | O : Nat
  | suc : Nat -> Nat.

From this definition, Coq automatically generates a recursor (aka an eliminator) for nat — an axiom giving the normal induction/recursion principles for , in a strong constructive form.

So it’s natural to ask if we can define the circle similarly, as the free type generated by a basepoint, and a path from that point to itself:

Inductive (Circle : Type) :=
  | base : Circle
  | loop : Paths base base.

Of course, Coq doesn’t accept this inductive definition — in normal inductive types, the constructors have to output elements of the type itself. So we have to axiomatise the type by hand. The type and its constructors are easy:

Axiom Circle : Type.

Axiom base : Circle.
Axiom loop : Paths base base.

What should the recursor look like? A map out of Circle into some other type should be specified simply by giving a point and a loop in that type; so as a first attempt, one might try:

Axiom circle_rec1 : forall (X : Type) (a : X) (l : Paths a a),
                       Circle -> X.

together with computation axioms stating that circle_rec1 X a l sends base to a and loop to l.

This is fine as far as it goes, and lets one prove a few things; but it corresponds only to, say, simple recursion on . To prove anything much about the circle, one needs something corresponding to full induction on — we need to be able to eliminate into a type dependent over Circle itself. So a second attempt might be:

Axiom circle_rec2 : forall (P : Circle -> Type)
                           (a : P base) (l : Paths a a),
                     forall (x : Circle), P x.

This was the first thing I tried originally… but a little thought shows it’s wrong! Why? Well, think topologically: we have a dependent type, so a fibration over the circle, for which we’re trying to give a section. A section doesn’t correspond to a loop in a fiber — which is what circle_rec2 asked for. A section corresponds to a loop lying over the whole circle down below — equivalently, to a point x, and a path in the fiber, to x, from the result of transporting x once around the circle.

(My TikZ skills are sadly not quite up to drawing tori yet!) So the actual recursor we want is:

Axiom circle_rec : forall (P : Circle -> Type) (a : P base)
                          (l : Paths (transport loop a) a),
                   forall (x : Circle), P x.

where we’ve previously defined the auxiliary function transport, or looked it up in our libraries:

 
Lemma transport : forall {X : Type} {P : X -> Type} {x x' : X}
                         (p : Paths x x'), (P x) -> (P x').

This is now the correct recursor; so we just need to add the computation axioms, and then we’ve got the circle:

Axiom circle_comp_base : forall (P : Circle -> Type) (a : P base)
                                (l : Paths (transport loop a) a),
                         Paths (circle_rec P a l base) a.

Axiom circle_comp_loop : forall (P : Circle -> Type) (a : P base)
                                (l : Paths (transport loop a) a),
         Paths (dependent_map_on_paths (circle_rec P a l) loop) l.

---

So, now that we’ve got the circle, what can we prove about it, or with it? Well, some simple first exercises:

• The circle is contractible if and only if UIP holds — that is, exactly if all types are discrete. (This holds in for instance the set-theoretic model: when all paths are trivial, the unit type satisfies the axioms of Circle.)
• Assuming Univalence, there is no path in Paths base base from loop to refl.

Less simply, but more interestingly, Mike Shulman has managed to prove:

• Assuming Univalence, Paths base base is equivalent to int. In other words, .

So, this seems to be a reasonable proposal for how to axiomatise the circle type-theoretically. But beyond that, the same idea which we used for the circle also gives us lots of other homotopy-theoretic constructions, in quite convenient and (it seems) type-theoretically natural forms. So I’ll end for now with a quick parade of these, giving just their imagined definitions as Coq inductive types, the explicit types of their recursors, and some notes on what one can do with them.

And, of course, you can pull down the Coq code and play with them yourself — the definitions below appear in full in Menagerie.v, in my fork of Andrej’s Homotopy repository.

Inductive Interval : Type :=
    | left : Interval
    | right : Interval
    | segment : Paths left right.

Axiom Interval_rect :
      forall {P : (Interval -> Type)}
             (d_left : P left)
             (d_right : P right)
             (d_segment : (transport segment d_left) ~~> d_right),
      forall x : Interval, P x.

Since one can prove that Interval is contractible, one might think there’s nothing interesting one can do with it. However, as Mike showed (and Chris Kapulkin noticed too), this implies functional extensionality, since it shows that paths are (in a weak sense) representable.

(That proof needs the computation rules to hold up to definitional equality, though; the version one can easily axiomatise in Coq, with the “computation” rules holding only up to homotopy, doesn’t imply this, since these axioms are all satisfied by the unit type. However, as Dan’s last post shows, there may be ways of getting around this.)

Inductive Circle : Type :=
    | base : Circle
    | loop : Paths base base.

Axiom Circle_rect :
         forall {P : (Circle -> Type)}
                (d_base : P base)
                (d_loop : (transport loop d_base) ~~> d_base),
         forall x : Circle, P x.

As mentioned above, one can show that Circle is contractible if and only if UIP holds; and one can show that the loop space of Circle at base is equivalent to the integers.

Inductive Circle' : Type :=
| east : Circle
| west : Circle'
| upper : Paths left right
| lower : Paths right left.

Axiom Circle'_rect :
forall {P : (Circle' -> Type)}
(d_east : P east) (d_west : P west)
(d_upper : (transport upper d_east) ~~> d_west)
(d_lower : (transport lower d_west) ~~> d_east),
forall x : Circle', P x.

An alternative presentation of the circle; proving this equivalent to Circle above is a nice exercise.

Inductive Sphere2 : Type :=
    | base2 : Sphere
    | surf2 : Paths (@refl base2) (@refl base2).

Axiom Sphere2_rect :
         forall {P : (Sphere2 -> Type)}
                (d_base2 : P base2)
                (d_surf2 : (transport (P := fun (p : base2 ~~> base2) => ((transport p d_base2) ~~> d_base2))
                            surf2 (idpath d_base2))
                            ~~> (idpath d_base2)),
         forall x : Sphere2, P x.

Sphere2 is contractible if and only if the principle “UIP-1” — that path spaces of path spaces are trivial — holds.

Inductive Susp (X : Type) : Type :=
    | north : Susp X
    | south : Susp X
    | merid : X -> Paths north south.

Axiom Susp_rect :
         forall {X : Type} {P : (Susp X) -> Type}
                (d_north : P north)
                (d_south : P south)
                (d_merid : forall x : X, (transport (merid x) d_north) ~~> d_south),
         forall x : Susp X, P x.

The suspension of a type. With this, one can define the spheres inductively, as a map from nat to Type.

Inductive Cyl {X Y : Type} (f : X -> Y) : Y -> Type :=
    | cyl_base : forall y:Y, Cyl f y
    | cyl_top : forall x:X, Cyl f (f x)
    | cyl_seg : forall x:X, Paths (intop x) (inbase (f x)).


Axiom Cyl_rect : forall {X Y} {f:X->Y} {P : forall y, Cyl f y -> Type},
                 forall (d_base : forall y:Y, P y (cyl_base y))
                        (d_top : forall x:X, P (f x) (cyl_top x))
                        (d_seg : forall x:X, (transport (cyl_seg x) (d_top x)) ~~> (d_base (f x))),
                 forall (y : Y) (z : Cyl f y), P y z.

This gives the mapping cylinder of any map of types. Intuitively, this gives the factorisation of any map into a cofibration followed by a trivial fibration.

(Triviality is the fact that for each y:Y, the type Cyl f y is contractible; proving this in Coq is again a nice exercise.)

In fact one can make this intuition precise — if a type theory admits “mapping cylinder types”, then its types carry classes of maps behaving just like the fibrations, cofibrations, and weak equivalences of a model structure. The fibrations are (generated by) dependent families of types; trivial fibrations, families of contractible types; cofibrations, constructos of (possibly higher) inductive types; trivial cofibrations, constructors of inductive types with a single constructor; and weak equivalences are exactly maps which are equivalences as defined in the type theory. (So the trivial cofibrations and fibrations of this “pre-model-structure” are exactly the Gambino-Garner weak factorisation system.)

Inductive isInhab (X:Type) : Type :=
    | proj : X -> isInhab X
    | contr : forall (y y' : isInhab X), Paths y y'.

Axiom isInhab_rect : forall {X:Type},
         forall {P : isInhab X -> Type}
                (d_proj : forall x:X, P (proj x))
                (d_contr : forall (z z' : isInhab X) (w : P z) (w' : P z'), (transport (contr z z') w) ~~> w'),
         forall z : isInhab X, P z.

This could be also described as , or : it gives a reflection from types into homotopy-propositions, squashing any type down to one which is contractible if it’s inhabited.

This is our first example that is “properly recursive”, with a constructor taking inputs from the inductive type itself.

Inductive tr0 (X:Type) : Type :=
    | incl : X -> tr0 X
    | contr : forall (l : Circle -> X),
                 Paths (refl (l base)) (cong l loop)

Similarly, with proper recursion, we can construct the 0-truncation, , aka , of any type; and this idea extends to give higher truncations as well. Here I’ve used a constructor whose arity is Circle; alternatively, one could also relax the restrictions on input types of constructors, to allow them to take paths directly as inputs:

Inductive tr0 (X:Type) : Type :=
    | incl : X -> tr0 X
    | contr : forall (z : tr0 X) (p : Paths z z), Paths p (refl z)

---

(A little bit of attribution: the basic idea of higher inductive types came from questions that were a lot in the air at Oberwolfach, and most immediately from discussions on the hike between Mike Shulman, Andrej Bauer, Michael Warren and myself. Since then, we and Chris Kapulkin have been playing with them further, and Dan Licata and Steve Awodey have independently been working on some closely related ideas, which I believe Dan is planning to post about soon…)