Homotopy Type Theory, VI
Posted by Mike Shulman
This will be the last post in this introductory sequence, although I will probably continue to post about new developments in homotopy type theory from time to time. (If you’re interested in the subject, you should also follow the HoTT blog.) Today I want to talk about a new, somewhat more radical idea, which we are currently calling higher inductive types.
The version of this I’m going to present below arose at Oberwolfach in discussions between Peter Lumsdaine, Andrej Bauer, Michael Warren, and myself, and since then Chris Kapulkin has also joined us in thinking about them. Peter did the initial implementation in Coq and noticed many of the applications below; a couple are my own inventions. (He also simultaneously wrote a post for the HoTT blog on the same subject.) I’m also told that Dan Licata and Steve Awodey have independently been working on related ideas. We all believe that this idea has the potential to solve many of the problems of homotopy type theory in a clean way, and one which moreover accords well with both type-theoretic and homotopy-theoretic intuition.
First, though, I should say a bit about ordinary inductive types. Categorically, an inductive type is a (perhaps weakly) initial algebra for an endofunctor. Intuitively, this means that it is freely generated by some collection of operations (possibly nullary, or parametrized by other types).
For instance, the natural numbers are freely generated by one point (zero) and one endomorphism (successor). Categorically, they are the initial algebra for the endofunctor , for which an arbitrary algebra is a type with a map , i.e. a point and an endomorphism .
I’ve so far avoided using “programmer’s syntax” in this sequence of posts, but with inductive types it becomes too cumbersome to do so, and it’s good to get some familiarity with how the code looks anyway. In Coq syntax, therefore, we can define the natural numbers as
Inductive nat : Type :=
| zero : nat
| succ : nat -> nat.
In Agda, we would write this as
data nat : Set where
zero : nat
succ : nat -> nat
We say that nat
has two constructors zero
and succ
, one of which takes no arguments and the other of which takes one argument of type nat
. The “inductiveness” of the definition comes from the fact that succ
takes an argument which is of the same type being defined. The universal property of nat
says that to define a function from nat
to , we just need to specify a point and an endomorphism . In Coq we would write the function defined in this way as
Fixpoint g (n : nat) : X :=
match n with
| zero => x
| succ n' => f (g n')
end.
while in Agda we would write it as
g : nat -> X
g zero = x
g (succ n') = f (g n')
In other words, if is zero, then , whereas if is the successor of , then .
The ability to define functions out of an inductive type like this is sometimes called its elimination rule. The fact that the value of at a given natural number can be computed using the data and which were used to define it is then called the computation rule. (There’s also a fancier version of the elimination rule, with a corresponding computation rule, in which the target type is allowed to be dependent on the inductive type such as nat
.)
An important thing to note is that in the presence of a universe, say “”, we can also define functions by recursion, and such functions are the same as types dependent on . Defining a dependent type by recursion is generally called “large elimination,” since is a “large object”.
Not all inductive types are “nontrivially recursive,” in the sense that the constructors take inputs of the type being defined. For instance, for any types and , their coproduct can be defined as an inductive type:
Inductive coprod (A B : Type) : Type :=
| inl : A -> coprod A B
| inr : B -> coprod A B.
(From now on I’ll give only the Coq syntax.) Here there are two constructors, one which takes an argument of type and one which takes an argument of type ; neither takes an element of the type being defined. In categorical terms, this means that we have an initial algebra for a constant endofunctor , which is of course just .
(In particular, note that identifying inductive types with algebras for endofunctors requires us to already know that the category in question has well-behaved coproducts. If we want to categorically construct coproducts as particular inductive types, as above, then we would need something more complicated, like joint-algebras for finite families of endofunctors. But if we work just in the type theory, then the elimination and computation rules for inductive types allow us to prove that coprod A B
is, in fact, a coproduct of and , and moreover that these coproducts are disjoint and stable under pullback. I mentioned this fact last time; see this comment thread.)
Identity types, or path types, are also a special kind of inductive type (or, more precisely, of inductive family). Their definition is
Inductive paths (A : Type) : A -> A -> Type :=
| idpath : forall (a : A), paths A a a.
This says that for each , there is exactly one constructor of , namely the identity path, and no other constructors. And the “elimination rule” for identity paths that I’ve mentioned before is exactly the elimination rule for this inductive family.
Now it may seem like there’s something a bit funny going on; how can there be nontrivial paths when we inductively require there to only be one of them? See this post and this one for a bit of insight into that question. It turns out that some kinds of inductive families, like path types, can “automatically” introduce nontrivial homotopy theory, whereas others, like natural numbers and coproducts, can’t. (In the latter case, one can actually prove that they can’t. For instance, defined as above is provably a set (i.e. a 0-type), and coproduct coprojections are provably injective and disjoint. Such proofs generally do require large eliminations, however.)
The basic idea of higher inductive types is to allow ourselves to explicitly introduce nontrivial homotopy theory in an inductive type, rather than “implicitly” as with identity types. Specifically, in the definition of inductive types and families, we allow also constructors which produce elements of (iterated) path types of the inductive type being defined, rather than elements of the type itself. For instance, here is a higher-inductive definition of .
Inductive circle : Type :=
| base : circle
| loop : paths base base.
That is, a circle is inductively generated by a point base
, and a path loop
from base
to itself. Its “elimination rule” says that to define a map , for any type , it suffices to give a point and a path from to itself. (As before, there’s also a fancier version where can be a type dependent on circle
.)
More generally, it is easy to see how to build any finite CW complex as a higher inductive type. Here is a 2-sphere:
Inductive sphere : Type :=
| base2 : sphere
| loop2 : paths (idpath base) (idpath base)
Here is a torus:
Inductive torus : Type :=
| base : torus
| meridian : paths base base
| equator : paths base base
| surf : paths (meridian @ equator) (equator @ meridian)
(I’m using @
to denote concatenation of paths, as in Andrej Bauer’s Coq files.) I think the ability to define these things is really important. Note that in all of our discussion so far, we’ve talked about doing homotopy theory, but we haven’t said anything about how to obtain the specific homotopy types we want to do homotopy with! Higher inductive types give us a straightforward and easy-to-work-with way to define such things.
But despite our suggestive naming, it seems that higher inductive types do not require the semantics to be nontrivially homotopical. For extensional semantics in a 1-category, no path-type admits any nontrivial loops, and so the “circle” is actually no different from a point. In fact, there is a converse too: by the universal property of the circle, if is contractible, then we can show that any two parallel paths, in any type, are equal (i.e. the type theory satisfies “UIP” or “axiom K”). So nontriviality of the circle encapsulates the nontriviality of the entire homotopy theory.
Therefore, univalence remains the only axiom we have (apart from the still-somewhat-nebulous quotient types) which guarantees the nontriviality of the homotopy theory of types. But is univalence alone sufficient to guarantee that all higher inductive types behave like the spaces we expect them to? A complete answer to this question would (it seems) require constructing a model which validates a general formulation of higher inductive types, which is still a question for the future, but we can obtain evidence for it by showing that specific higher inductive types behave in expected ways.
As one step in this direction, I was recently able to show (and formalized in Coq) that assuming the univalence axiom, we have , where is the circle type defined inductively as above. Since is a set, it is its own , so this also implies . (This might be the first actual computation of a nontrivial homotopy group in homotopy type theory; I am not sure.) I also have confidence that homotopy type theory admits enough homotopical machinery, such as fibration sequences, to allow us to compute more familiar homotopy groups.
Here is another higher inductive type, perhaps even simpler than the circle:
Inductive interval : Type :=
| zero : interval
| one : interval
| segment : paths zero one.
That is, an interval is inductively generated by two points, zero and one, and a path between them. Its (non-dependent) elimination rule says that to define a map , for any type , it suffices to give two points and a path .
Of course, in homotopy theory an interval is contractible, and we can also prove this in homotopy type theory about the interval thusly defined. So you might think the interval type doesn’t buy us very much. But actually it does, because it makes homotopies “representable”; in homotopy-theoretic language, it is (unsurprisingly) an interval object. One consequence of this, which occurred to me in the midst of this discussion, is that as long as the computation rules for the interval are “definitional” (i.e. holds on the point-set level in the category of types, rather than only up to homotopy), we can prove function extensionality; see this post.
This suggests a way to think about higher inductive types in general: they supply the “left side” of homotopy theory which has so far been missing. The “right side” of homotopy theory, having to do with fibrations, is well-modeled in homotopy type theory: we have a weak factorization system analogous to (acyclic cofibrations, fibrations), we have a good notion of fibrations (= display map = dependent type) which is preserved by pullback, all objects are fibrant, and we have path objects. However, we have said nothing about a notion of cofibration, cofibrant objects, cell complexes, cylinder objects, or a (cofibration, acyclic fibration) factorization system. Higher inductive types supply all of these deficiencies.
For instance, in addition to CW complexes like spheres and tori, we can also build “parametrized cell complexes” by using constructors that take other types as inputs. Here is a cylinder type:
Inductive cylinder (A : Type) : Type :=
| inl : A -> cylinder A
| inr : A -> cylinder A
| seg : forall (a : A), paths (inl a) (inr a)
While the cylinder type will be equivalent to , just like the interval type was contractible, it has the homotopy-theoretic property of a cylinder object: maps out of it represent homotopies between functions , just like maps into the path object represent homotopies between functions .
Similarly, here is the homotopy pushout of two functions and :
Inductive hpushout {A B C : Type} (f : A -> B) (g : A -> C) : Type :=
| inl : B -> hpushout f g
| inr : C -> hpushout f g
| glue : forall (a : A), paths (inl (f a)) (inr (g a)).
That is, the pushout of and is inductively generated by a map from , a map from , and a path between the images of and of for any . Similarly, we can expect to be able to construct any particular kind of finite homotopy colimit.
Lastly in this vein, we can construct mapping cylinders, as essentially a special case of the homotopy pushout:
Inductive mcyl {A B : Type} (f : A -> B) : Type :=
| inl : A -> mcyl f
| inr : B -> mcyl f
| mseg : forall (a : A), paths (inl a) (inr (f a)).
Of course, as usual the mapping cylinder will be homotopy equivalent to , but again it has a homotopy-theory value: it gives us the other weak factorization system, by the following argument.
Recall that identity types (or, more generally, inductive families) give us (according to Gambino and Garner) one WFS on the category of types, in which the right class of maps is (generated by) the projections from dependent types, which we call “display maps”. This WFS is like the (acyclic cofibration, fibration) factorization system in a model structure. A generating class of acyclic cofibrations is the singleton constructors: the constructors of inductive types that have only one constructor. To see this, consider a square
in which is a singleton constructor and a display map. We must define a map such that and . But since is an inductive type and its only constructor, to define a map it suffices to give its composition with , namely ; then we will have by definition, and will follow from .
Now we also have a natural class of weak equivalences, namely the homotopy equivalences, and we can characterize the acyclic fibrations: a display map is an equivalence iff each type is contractible (in a way continuously parametrized by , i.e. ). If we suppose that , above, has this property, then what additional maps satisfy the lifting property with respect to it?
It turns out that the answer is arbitrary constructors of (possibly higher) inductive types. For if is any constructor of an inductive type, to define it suffices to define its value constructor-by-constructor. On the particular constructor we can do as before, while for any other constructor we can use the continuous contractibility of the fibers of to select a point in the necessary fiber, making the lower triangle commute. (The value of on constructors other than has no effect on commutativity of the upper triangle.)
Now that argument looks as though it only requires the fibers of to be (continuously) inhabited, i.e. for to be split epic. And, indeed, we should have a WFS looking something like (constructors of inductive types, split-epic display maps). However, we need to be an acyclic fibration if we want it to also have the lifting property with respect to constructors of higher inductive types. For in that case, there may be paths in which connect points arising from different constructors, and to define on these paths, we need to use contractibility of the fibers of .
Thus, it makes sense to take as (generating) cofibrations the class of constructors of (higher) inductive types. All that’s missing to obtain a WFS in this way, therefore, is a factorization of an arbitrary map into a cofibration followed by an acyclic fibration. The mapping cylinder will give us this, if we modify it a bit so that it gives an output which is dependent on the codomain:
Inductive mcyl {A B : Type} (f : A -> B) : B -> Type :=
| inl : forall (a : A), mcyl f (f a)
| inr : forall (b : B), mcyl f b
| mseg : forall (a : A), paths (inl a) (inr (f a)).
We can then go through some standard model-categorical retract-argument business to conclude that these two WFS actually form a model structure on the category of types (modulo the defect that it lacks limits and colimits). Peter Lumsdaine has written out a proof.
So far I’ve argued that higher inductive types supply the “missing half” of homotopy theory, and in particular allow us to construct familiar spaces like spheres, tori, projective spaces, Lie groups, etc: anything that can be given a finite cell structure. (With some cleverness, we can probably construct at least some infinite cell complexes as well.) But really, we haven’t even scratched the surface yet, because none of our “higher inductive types” have been “honestly recursive” yet—none of their constructors have taken any inputs from the type being defined!
The most impressive application of “honestly recursive” higher inductive types that I’ve seen so far is the following.
Inductive supp (A : Type) : Type :=
| proj : A -> supp A
| contr : forall (x y : supp A), paths x y.
What does this mean? The type comes with a map proj
from , and moreover the type is inhabited. But the latter is actually an equivalent way to say that is a (-1)-type, i.e. contractible if inhabited. Furthermore, the elimination rule for says that if is another (-1)-type equipped with a map from , there is a canonical map . In other words, is , the (-1)-truncation of !
I think this is, without a doubt, the cleanest construction of the (-1)-truncation I’ve ever seen; I was very excited when Peter showed it to me. We can apply a similar idea “pathwise” to construct higher truncations as well:
Inductive pi0 (A : Type) : Type :=
| proj : A -> pi0 A
| contr1 : forall (x y : pi0 A) (p q : paths x y), paths p q.
Thus has a map from and is a 0-type (each of its hom-types are (-1)-types), and is universal among such. We can now define things like
We can use a similar idea to construct a certain amount of quotients, as discussed in the last post. For instance, if is an equivalence relation on a set , which is in particular a (-1)-type dependent on , then we might think its quotient should be something like
Inductive quotient (A : Type) (R : A -> A -> NType (-1)) : Type :=
| proj : A -> quot A R
| relate : forall (x y : A), R x y -> paths (quot x) (quot y)
| contr1 : forall (x y : quot A R) (p q : paths x y), paths p q.
This says that is a set (a 0-type) universally equipped with a map from and a path relating the images of any two points for which holds. This should give it the correct universal property in the category of sets, at least, and we might even be able to prove that is the kernel of . But I don’t immediately see a way to show that this has the right universal property for mapping into types that aren’t 0-types. (On the other hand, if we can be sure that a set having this stronger universal property exists, then it should be equivalent to defined as above.)
In a similar way, we should be able to construct “quotients” of groupoids composed of -types, which have the right universal property relative to other -types, for any fixed (external) natural number ; so the only thing standing in the way of constructing all quotients using higher inductive types is infinity. If we allowed higher inductive types with infinitely many constructors, then I have no doubt that we could define honest quotients of any internal groupoid. This gives me a certain amount of hope that once we have a manageable finitary definition of “internal groupoid”, we may be able to use higher inductive types to construct actual quotients thereof.
On the other hand, as far as I can tell, higher inductive types are not subsumed by quotients for groupoids, although they can accomplish some of the same purposes (like truncation, and at least some colimits). For instance, the circle can be constructed as the quotient of the groupoid , but constructing a groupoid whose quotient would be seems no easier than constructing itself. (Remember that is not !)
I hope I’ve convinced you that higher inductive types are a fruitful direction for further development of homotopy type theory. However, I want to end with a few caveats.
The formal foundation of this is still a bit in flux. For particular higher inductive types, like the interval, the circle, the mapping cylinders, and so on, we can write down elimination and computation rules that we’re pretty sure are correct. It isn’t appropriate to get into the details here, but you can look at Peter Lumsdaine’s post on the HoTT blog for the form of these rules (including the dependent elimination rules). However, what hasn’t quite solidified yet is a completely general formulation of “a higher inductive type” — what’s allowed, what isn’t, and what elimination and computation rules you end up with.
While we obviously have intuition about what these types should look like in homotopy models, there is work to be done in constructing such types so as to satisfy all the type-theoretic rules. We do know how to find models explicitly in some simple cases. For instance, it’s not hard to show that in the 1-groupoid model of type theory, the groupoid satisfies the rules for the circle type.
We need to investigate their computational behavior. In ordinary type theory, computational behavior (such as normalization and termination) is at least as important as the existence of models.
Unfortunately, none of this actually works in Coq or Agda (yet) exactly as written. But we can mostly fake it, by asserting any particular higher inductive type as an axiom, along with its constructors, elimination rule, and computation rules. Some examples are available in Peter’s HoTT post. This is how those of us working on this idea have been formalizing things so far.
I say we can “mostly” fake it, because in this way we can generally only make the computation rules hold up to homotopy. This is enough for many purposes (although it makes things a good deal more cumbersome), but not for others (in particular, it is insufficient for the proof of function extensionality from an interval type). However, Dan Licata has a clever hack which allows the computation rules for points (but not for paths) to hold on the nose.
Re: Homotopy Type Theory, VI
This stuff is great. I think you guys are coming close to the promised land where logic, -groupoids and homotopy theory become inseparable and even easy to explain.