(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…)

Do you mind giving the definition of your

dependent_map_on_pathsmorphism? I’ll admit i’m having a bit of trouble working it out on my own.Well, the type of it is:

(I tend to think of the target type here as “paths from

f(x)tof(y)lying overp”.) Now that it’s stated in enough generality, you can just induct onpto 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.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

computationrule, 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…?Would a computational interpretation of univalence make a difference here, i.e. would it help with the auxiliary terms?

I’m not sure what univalence would have to do with it… did you have something in mind?

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 ofpaths in the total space lying overthe path`p : x ~~> y`

in the base space.