Higher Inductive Types

Higher Inductive Types via Impredicative Polymorphism

The proof assistant Coq is based on a formal system called the “Predicative Calculus of (Co)Inductive Constructions” (pCiC). But before pCiC, there was the “Calculus of Constructions” (CoC), in which inductive types were not a basic object, but could be defined using impredicative polymorphism (i.e. universal quantification over a universe when defining a type existing in that same universe). In fact, higher inductive types can be defined in the same way (although this approach suffers the same drawbacks for higher inductive types as it does for ordinary ones).

As a basic example of how to define inductive types impredicatively, the natural numbers can be defined as

In other words, a natural number is a polymorphic function which assigns, to every type C equipped with a point (z, say) and an endomorphism (f, say), an element of C. One can then define

In other words, zero assigns z to every type C as above, while succ n asks what n would assign, then applies f to it. For these definitions one can then prove the non-dependent elimination rule for , which satisfies its computation rule definitionally.

The current Coq system does not allow impredicative definitions by default, but it can be told to allow them (in the lowest universe Set) with the command-line argument -impredicative-set. Thus, in Coq with -impredicative-set, we can write the above definitions as

Definition nat : Set := forall (C:Set), C -> (C -> C) -> C.

Definition zero : nat := fun C z f => z.

Definition succ : nat -> nat := fun n C z f => f (n C z f).

It is perhaps not surprising that we can define higher inductive types as well using impredicative polymorphism. Here is an interval:

Definition interval : Set :=
  forall (X : Set) (a b : X) (p : a ~~> b), X.

That is, an element of the interval is a polymorphic function which assigns, to any type X equipped with two points a, b, and a path p between them, a point of X. Note that this path type (a ~~> b is notation for paths a b) denotes the honest inductive family defined as usual, not its stand-in defined as above using impredicative polymorphism; thus this is actually a definition in CiC, the impredicative Calculus of (Co)Inductive Constructions. We could use the impredicatively defined path-type, but I doubt we could prove interval_compute_segment, below, without dependent elimination for paths.

The endpoints of the interval are easy to define.

Definition zero : interval := fun X a b p => a.

Definition one : interval := fun X a b p => b.

The path between them is also straightforward, but since zero and one are now both functions, we need (dependent) functional extensionality.

Axiom funext_dep :
  forall (X : Type) (P : X -> Type) (f g : forall x : X, P x),
    (forall x : X, f x ~~> g x) -> f ~~> g.

Definition segment : zero ~~> one.
Proof.
  apply funext_dep with (f := zero) (g := one); intro X.
  apply funext_dep; intro a.
  apply funext_dep; intro b.
  apply funext_dep; intro p.
  unfold zero, one; exact p.
Defined.

Defining the recursor is easy:

Definition interval_rec :
  forall (X : Set) (a b : X) (p : a ~~> b), interval -> X :=
  fun X a b p i => i X a b p.

and it follows, as for ordinary inductive types, that the computation rules for the endpoints hold definitionally. Thus, we can prove function extensionality from eta (although it’s pretty silly to do so, since we needed to assume functional extensionality to define the interval in this way).

Axiom eta_dep_rule :
  forall (A : Type) (P : A -> Type) (f : forall x : A, P x),
    (fun x => f x) ~~> f.

Theorem interval_implies_funext_dep :
  forall (X : Set) (P : X -> Set) (f g : forall x : X, P x),
    (forall x : X, f x ~~> g x) -> f ~~> g.
Proof.
  intros X P f g p.
  set (mate := fun (i:interval) x => interval_rec _ _ _ (p x) i).
  path_via (mate zero).
  apply opposite.
  path_via (fun x => f x).
  apply eta_dep_rule.
  path_via (mate one).
  exact (map mate segment).
  path_via (fun x => g x).
  apply eta_dep_rule.
Defined.

The one thing missing is the computation rule for the segment:

Definition interval_compute_segment :
  forall (X : Set) (a b : X) (p : a ~~> b),
    map (interval_rec X a b p) segment ~~> p.

The proof is long, straightforward, and unenlightening, so I won’t post it, but I will note that I needed to use the “computation rule” for function extensionality:

Axiom funext_dep_compute :
  forall (X : Type) (P : X -> Type) (f g : forall x : X, P x)
    (p : forall x : X, f x ~~> g x) (x : X),
    happly_dep (funext_dep X P f g p) x ~~> p x.

This is obviously a sensible thing to require. Moreover, Voevodsky proved that assuming funext_dep as above, one can find a (possibly) different inhabitant of the same type as funext_dep which does satisfy funext_dep_compute, so it is harmless to assume it.

So what does this tell us about higher inductive types? Note, first, that as for ordinary inductive types, we cannot (as far as I know) deduce the dependent version of the elimination rule in this way. And as for ordinary inductive types, the dependent elimination rules are really essential to the theory. For instance, they are necessary in order to prove that the interval is contractible, and in order to calculate . So as far as I can tell, this is not a good way to implement HITs in practice.

However, I think this construction does provide additional evidence that HITs are “reasonable gadgets”. In particular, a type theorist should not think of HITs as a weird or radical thing that the homotopy theorists dreamed up. (-:

Instead, we can think about them as follows. The original CoC with impredicative Set allows the definition of inductive types, but was insufficient to prove all of their desired properties; hence first-class inductive types were introduced (and can also be added to a predicative theory). With HITs, we notice a somewhat more general class of definitions that we can make in CiC with impredicative Set (after adding first-class inductive types to CoC), but which again have desired properties that are not provable there (and are also predicative); hence we again need to make them first-class objects.

I also like this construction because identity types have no special role in the impredicative CiC. Perhaps there is a larger class of permissible definitions in CiC, which includes HITs but which can be defined without giving identity types any special role, and which we should try to make into first-class predicative objects with “dependent eliminators.”

On the other hand, I don’t know whether anyone has constructed a homotopy or groupoid model for impredicative CoC with identity types; is impredicative CoC even known to be consistent with the negation of UIP?