Higher Inductive Types: a tour of the menagerie

(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 \mathbb{N}, 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 \mathbb{N}. To prove anything much about the circle, one needs something corresponding to full induction on \mathbb{N} — 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.

Sections of a fibration over 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, \Omega(S^1,x_0) \cong \pi_1(S^1,x_0) \cong \mathbb{Z}.

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 \text{tr}_{-1}, or \pi_{-1}: 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, \mathrm{tr}_0, aka \pi_0, 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…)

About these ads
This entry was posted in Code, Higher Inductive Types. Bookmark the permalink.

7 Responses to Higher Inductive Types: a tour of the menagerie

  1. cody says:

    Do you mind giving the definition of your dependent_map_on_paths morphism? I’ll admit i’m having a bit of trouble working it out on my own.

    • Well, the type of it is:

      Definition dependent_map_on_paths 
                    {A} {P : A -> Type} (f : forall x : A, P x) 
                    {x y : A} (p : x ~~> y)
                  : transport p (f x) ~~> f y.
      

      (I tend to think of the target type here as “paths from f(x) to f(y) lying over p”.) Now that it’s stated in enough generality, you can just induct on p to finish the job. I won’t elaborate more here — it’s a good exercise — but if you want the full codes, it’s near the beginning of Menagerie.v on my Github.

  2. Bas Spitters says:

    Is it clear how to extend the iota-rule?

    • No, not quite! (The iota-rule is the CoC name for what the M-L tradition calls computation rules, is that right?) As far as I can see there are two main choices to make.

      First, for the “0-constructors”, one can ask the computation rule to hold either definitionally or propositionally. It seems quite natural to ask for it definitionally, just like for ordinary inductive types; and it’s definitely stronger to ask for it definitionally, as the proof of functional extensionality from the interval shows. (The propositional-computation version of the interval rules is satisfied by a unit type, so certainly can’t prove functional extensionality.)

      Second, there’s the same choice for higher constructors. Here, I’m not at all sure whether one should ask for it definitionally or just propositionally. On the one hand, seeing them as inductive types, it seems reasonable to look at it as a computation rule, an actual reduction. On the other, since the “redex” now involves somewhat non-canonical auxiliary terms, like what I’ve called here dependent_map_on_paths (aka cong etc.), whose own behaviour under composition etc. is typically only well-behaved up to homotopy, in practice there’s not much gain from it; and perhaps it isn’t so natural after all…?

    • Mike Shulman says:

      For the moment, propositional computation rules have the advantage that we can assert them as axioms in Coq, so that’s what we’re using. Dan Licata’s trick gives us definitional computation rules for the 0-constructors in Agda, but not for the higher constructors, and its applicability in Coq is questionable.

      On the other hand, apart from the definitional/propositional choice, there should definitely be an algorithmic way to extract the computation rule from the “inductive specs” that Peter gave above. But making this precise in generality (and, indeed, making precise what sort of “inductive specs” are allowed) is work in progress. I think the key is likely to be the idea that Peter alluded to above: that the type transport p z ~~> w, for points z : P x and w : P y in two different fibers of a fibration, should be regarded as the type of paths in the total space lying over the path p : x ~~> y in the base space.

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s