Directed Homotopy Type Theory
Posted by Mike Shulman
Recently I’ve been talking a lot about homotopy type theory, and its potential role as a foundation for mathematics in which homotopy types — which is to say -groupoids — are basic objects. However, when I say this to -categorists, I inevitably get the question “Why stop with -groupoids? What about -categories, or -categories, or -categories?” Until now, I’ve had only two answers:
Maybe there is a foundation in which higher categories are basic objects — but we don’t know yet what it might look like. For instance, some of us have thought about a “directed type theory” for 1-categories. This seems to work, but it’s not as clean as homotopy type theory: the composition laws seem to have to be put in by hand, rather than falling out automatically like they do for -groupoids using the inductive definition of identity types. For -categories or -categories, it seems that we would essentially have to build something like a Batanin operad into the structure of the type theory. This is probably possible, but not especially appealing to me, unless someone finds a clean way of “generating” such an operad in the same way that Martin-Löf identity types “generate” all the structure of a Batanin -groupoid.
There is also the question of what a “dependent type” should mean for directed categories. Presumably some sort of fibration — but of what variance? We seem to need different kinds of “dependent type” for fibrations and opfibrations, and as we go up in categorical level this problem will multiply itself. Moreover, not all functors are exponentiable, so dependent product types will require some variance assumptions. Furthermore, I think there are some issues with the categorical semantics when you get up to 3-categories: comma objects don’t seem to do the right thing any more.
These problems suggest that maybe even in the long run, we’ll decide that it’s better to only build -groupoids into the foundational system, with directed categories as a defined notion. (I’m not saying I think we necessarily will, just that I think it’s possible that we will.) If we go this route, then I think the most promising way to define -categories inside homotopy type theory would be an adaptation of Charles Rezk’s “complete Segal spaces” and -categories, since these are defined entirely in terms of diagrams of -groupoids and don’t require any truncatedness of the space of objects. (The fact that every -groupoid admits an essentially surjective map from a 0-truncated one — that is, from a set — is a “classicality” property that doesn’t hold in general homotopy type theory. Thus, any definition of -categories which requires that the objects form a set — which includes most definitions other than Rezk’s — would be insufficiently general.)
However, we don’t yet know how to define simplicial objects or -objects inside of homotopy type theory (unless we are willing to allow infinite lists of definitions, which is fine mathematically if we assume a strong enough metatheory, but difficult to implement in a computer). Depending on how we end up solving that problem, this approach could also turn out to be technically complicated.
In this post, I want to present a third approach, which sort of straddles these two pictures. On the one hand, it gives us a way to talk about -categories (and, probably, -categories) inside homotopy type theory today, without waiting for a solution to the problem of defining simplicial objects (although in the long run, we’ll still need to solve that problem). On the other hand, we can think of it as a rough approximation to what an eventual “directed homotopy type theory” might look like.
However, this is still just a basic idea; there are technical issues as well as conceptual questions that need to be answered. I’ve been rolling them around in my head for a while and not making much progress, so I’m hoping to start a discussion in which other people may be able to see what I can’t.
The point is simply this: complete Segal spaces (which some of us might prefer to call something like “Rezk categories”) are, in particular, simplicial -groupoids. However, the -category of simplicial -groupoids is, itself, an -topos. Therefore, we can interpret homotopy type theory internally to it. The plan, therefore, is to work in the internal homotopy type theory of , as a place to talk about -categories (incarnated as Rezk categories).
Of course, for this to work, we’ll need to make some of the special structure of visible in its internal homotopy type theory. The most important observation is that is the classifying topos of 0-truncated total orders with distinct endpoints (a.k.a. “strict intervals”). The corresponding fact for the 1-topos of simplicial sets is classical and due to Joyal (it’s described in “Sheaves in Geometry and Logic”), and the extension to is easy: the main thing to notice is that a flat functor from a 1-category to an -category must land in the 0-truncated objects.
Thus, a basic property of the internal homotopy type theory of will be the presence of the generic 0-truncated strict interval. A 0-truncated strict interval is easy to axiomatize; here’s some Coq:
Axiom I : Type.
Axiom I_is_set : is_set I.
Axiom Ile : I -> I -> Type.
Axiom Ile_is_prop : forall x y, is_prop (Ile x y).
Axiom Ile_refl : forall x, Ile x x.
Axiom Ile_trans : forall x y z, Ile x y -> Ile y z -> Ile x z.
Axiom Ile_antisym : forall x y, Ile x y -> Ile y x -> x == y.
Axiom Ile_total : forall x y, is_inhab ((Ile x y) + (Ile y x)).
Axiom bot : I.
Axiom top : I.
Axiom bot_ne_top : (bot == top) -> Empty_set.
Axiom bot_Ile : forall x, Ile bot x.
Axiom Ile_top : forall x, Ile x top.
Speaking internally, there’s no way to axiomatically ensure that this order is the generic one. Fortunately, we don’t need to; even just this amount of structure is sufficient for a whole lot. Moreover, the extra generality is useful: it means we aren’t restricted to semantics in itself. In particular, we could be in for any -topos , so that the theory applies to internal (infinity,1)-categories in any -topos.
Using the directed interval object I
, we can define the standard simplices, the simplicial operators, and the maps between the standard simplices that they induce. For instance, the standard -simplex is the subtype of the -fold product that consists of the ordered tuples . There are various ways to define the simplicial operators; I chose an inductive definition, which seemed convenient at the time, but perhaps simply using order-preserving functions between finite types would be easier.
Now, for any type , the type of -simplices in is . In particular, the type of -simplices in can also be called the type of morphisms in , while the type of -simplices is equivalent to itself. We have a “source and target” map induced by precomposing with top
and bot
, and the (homotopy) fiber of this map over can be called . Similarly, putting together a bunch of simplicial operators, we can inductively define the Segal maps
It’s then tempting to define to be a Segal type if these maps are equivalences, i.e.
We always have to be careful when doing this sort of thing, though, to make sure that our naive “external” ideas “internalize” correctly. In this case, since our “types” are now secretly simplicial spaces, each is itself a simplicial space, not just a space, and so is asking a bunch of maps of simplicial spaces to be (levelwise) equivalences. The external space of 0-simplices of is the external space of -simplices of , so if holds internally, that at least implies that is a Segal space externally.
In fact, I believe that in this case, says no more than that is an external Segal space. Being a Segal space is the same as being local with respect to some maps , whereas should be asserting also locality with respect to for all . But Charles Rezk proved that if is a Segal space, then so is for any simplicial space (that is, Segal spaces are an exponential ideal), and in particular so is . Thus, this stronger property should follow automatically by adjointness.
Now in a Segal type, we can define composition in the usual way, by applying the inverse of and then the diagonal operator . We have an identity-assigning map coming from degeneracies, and we can define what it means for an element to be an internal equivalence. To make this property into an h-proposition, we need to phrase it using adjoint equivalences or h-isomorphisms, as usual. (In this case, Voevodsky’s definition of equivalence — all homotopy fibers are contractible — is not available, since is not a function in type theory.) And as usual, h-isomorphisms seem to be an easier choice.
Finally, every identity is an internal equivalence, so the degeneracy map factors through . Thus, we can define a Segal type to be a Rezk type, or a category, if this map is an equivalence. Since Rezk categories are also an exponential ideal, this should also characterize the correct objects externally.
An equivalent way to define Rezk types is to first define a dependent equivalence-type . Then path-elimination gives us an “internal path-to-equiv” morphism , which we can ask to be an equivalence. Thus we see that as Urs pointed out recently, Rezk-completeness is a generalized sort of “univalence axiom”.
The notion of -category that we get in this way is an interesting hybrid of existing definitions. Obviously, it mimics the “simplicial, nonalgebraic” notion of Rezk category at the top level. However, the underlying “spaces” are not simplicial sets or topological spaces, but types in homotopy type theory, which (notwithstanding that we generally model them categorically using simplicial sets) behave internally more like a globular, algebraic sort of -groupoid: their iterated path-types form a globular set which is acted on by a contractible globular operad. Moreover, even the “Segalic/nonalgebraic” top level is “algebraically nonalgebraic”, in the sense I described at the end of this post.
This approach also pleasingly reifies the notion that categories are “directed spaces”. If we think of ordinary homotopy type theory as a “theory of spaces”, then what we’ve done here is axiomatically specify a “basic directed path”, so that we can define the “directed paths” in any other space by mapping out of it. Evidently, from this point of view, not every “directed space” is a category: we need the Segal condition and the Rezk completeness condition to make a directed space behave like a category.
Finally, there is an obvious way to generalize to -categories, by working in the -topos of cellular spaces rather than simplicial spaces, and mimicking Rezk’s Theta-spaces rather than complete Segal spaces. I believe that when Joyal introduced the category , he proved that presheaves on are the classifying topos for some theory generalizing strict intervals (called “disks” of some sort?). Thus, it seems likely that this approach would generalize in a straightforward way.
There are two main problems that I’ve been puzzling about and not making much progress. First of all, there is lots of other structure on that we might want to include as well. For instance, it is a cohesive -topos. We’ve discussed before how to axiomatize cohesiveness internally. One nice thing in this case is that since we know what the discrete and codiscrete objects are, we don’t need to axiomatize them abstractly; we can define them in terms of the standard simplices.
The codiscrete objects are the “0-coskeletal” ones: those where is an equivalence for all . This is of course equivalent to being local for the inclusions . Since the codiscrete objects are an exponential ideal, this localization is an “internal” one, and so it can be defined in the internal type theory. Moreover, the localization itself (the codiscrete reflection ) can be constructed as a higher inductive type, rather than needing to be asserted axiomatically (as is the case for a general cohesive topos). However, I think we would probably have to assert axiomatically that this localization is left-exact.
More generally, for a map we have if and only if the square is a pullback (as always in a cohesive topos). In this case, that means that the map of simplicial objects is uniquely determined (externally) by a map of non-simplicial objects.
The discrete objects are the constant ones: those where each simplicial operator is an equivalence. As remarked in this post, since the discrete objects are also an exponential ideal, they can also be described internally as a reflective subfibration. However, there may be different such reflective subfibrations with the same underlying exponential ideal. One such reflective subfibration would be obtained by localizing internally at all the simplicial operators acting on standard simplices. Is that a good one to work with? Are there any better ones?
It also seems that the discrete objects should be exactly the Rezk types in which all morphisms are invertible. However, I haven’t tried to prove this formally yet. (Note that codiscrete objects are almost never even Segal types.)
There should also be various interesting subtypes of the universe , which should be able to tell us something about all the different sorts of “dependent type” that can exist in the directed situation. Some of them we can construct from the directed interval, while others will probably have to be asserted axiomatically separately.
From the cohesive structure, we have the “type of codiscrete objects” . Since the codiscretes are left-exact reflective, this is itself codiscrete. It is also a full subtype of , i.e. maps to it by a (-1)-truncated morphism. Externally speaking, it is the -groupoid of -groupoids, regarded as a codiscrete simplicial -groupoid (which is not the same as regarding it as an -category and incarnating it as a Rezk type; remember that codiscrete simplicial objects are almost never Segal). Maps from into it classify “relatively codiscrete” maps as above.
Any particular choice of a reflective subfibration that extends the discrete objects will also give us a full subtype of . Is there a choice for which we get something interesting here? What kind of maps are classified by this?
Since Segal types and Rezk types are also exponential ideals, we can extend them to reflective subfibrations that will also be classified by full subtypes of . Looking at small examples has suggested to me that if we make the obvious choice for Rezk types, we get a classifier for maps which are “Grothendieck constructions of morphisms into partial profunctors”. By this I mean that the fiber of over each 0-simplex of is a Rezk type, and the fiber over each 1-simplex is a “partial profunctor” in which the morphisms on both sides may or may not act, but insofar as they do act, they act associatively. It would be nice to find a precise description of these morphisms; perhaps they are related to the fibrations in the model structure for Rezk categories.
We can also take various familiar -categories, incarnate them as Rezk categories, and see what they look like internally. The most obvious choice is itself, which should be a classifier for “Rezkian Cartesian opfibrations” (and similarly, should classify Rezkian Cartesian fibrations). But what is the definition of such a thing? And what is the best way to axiomatize internally the existence of classifiers for them? Will it include some sort of “directed univalence axiom”?
Similarly, we have and , incarnated as Rezk categories. I believe that will be a classifier for the sorts of fibrations that Charles mentions in his answer to this question, and of course is dual.
Finally, there is the problem of formalizing all of this in a proof assistant. Up above I wrote down the axioms of the directed interval in Coq. I’ve managed to do a fair amount with these axioms, including defining all the standard simplices and the simplicial operators. This suffices for the definition of Segal types; see here. Unfortunately, the simplicial operators we get are only functorial up to homotopy. The homotopies are coherent (easily, because the directed interval is -truncated), but they still have to be handled explicitly in Coq. This leads to lots of extra paths and transport
s flying around and things get extremely messy.
So far, I have not managed to prove even that composition in a Segal type is associative and unital. It’s “obvious” how to go about it, using the higher Segal conditions, but so far the technical obstacles have been too overwhelming for me to push it through. I’m hoping that there is some trick that I just haven’t thought of yet which will make this feasible. Perhaps I made poor choices in defining the simplices and simplicial operators, and a better choice would make the technical obstacles go away. Any ideas, anyone?
Re: Directed Homotopy Type Theory
I am so glad to see that you are pushing this, with success!
I am also happy to see that you are going via internal characterization of the -topos of simplicial objects. Something like this is what I tried to play around with (very unsuccessfully) in a recent Forum thread on classifying toposes of intervals. That approach “feels right” to me.
While this post catches me in the middle of the night when I just wanted to go offline, let me ask one quick question (having only scanned your post so far, admittedly):
with the structure you have here, can you construct the “self-indexing” as an internal category from the type classifier, i.e. the “small self-reflection of the topos”?