Skip to the Main Content

Note:These pages make extensive use of the latest XHTML and CSS Standards. They ought to look great in any standards-compliant modern browser. Unfortunately, they will probably look horrible in older browsers, like Netscape 4.x and IE 4.x. Moreover, many posts use MathML, which is, currently only supported in Mozilla. My best suggestion (and you will thank me when surfing an ever-increasing number of sites on the web which have been crafted to use the new standards) is to upgrade to the latest version of your browser. If that's not possible, consider moving to the Standards-compliant and open-source Mozilla browser.

June 7, 2012

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 \infty-groupoids — are basic objects. However, when I say this to nn-categorists, I inevitably get the question “Why stop with \infty-groupoids? What about nn-categories, or (,n)(\infty,n)-categories, or (,)(\infty,\infty)-categories?” Until now, I’ve had only two answers:

  1. 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 \infty-groupoids using the inductive definition of identity types. For nn-categories or ω\omega-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 \infty-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.

  2. These problems suggest that maybe even in the long run, we’ll decide that it’s better to only build \infty-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 (,n)(\infty,n)-categories inside homotopy type theory would be an adaptation of Charles Rezk’s “complete Segal spaces” and Θ\Theta-categories, since these are defined entirely in terms of diagrams of \infty-groupoids and don’t require any truncatedness of the space of objects. (The fact that every \infty-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 (,n)(\infty,n)-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 Θ\Theta-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 (,1)(\infty,1)-categories (and, probably, (,n)(\infty,n)-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 \infty-groupoids. However, the (,1)(\infty,1)-category (Gpd) Δ op(\infty Gpd)^{\Delta^{op}} of simplicial \infty-groupoids is, itself, an (,1)(\infty,1)-topos. Therefore, we can interpret homotopy type theory internally to it. The plan, therefore, is to work in the internal homotopy type theory of (Gpd) Δ op(\infty Gpd)^{\Delta^{op}}, as a place to talk about (,1)(\infty,1)-categories (incarnated as Rezk categories).

Of course, for this to work, we’ll need to make some of the special structure of (Gpd) Δ op(\infty Gpd)^{\Delta^{op}} visible in its internal homotopy type theory. The most important observation is that (Gpd) Δ op(\infty Gpd)^{\Delta^{op}} is the classifying topos of 0-truncated total orders with distinct endpoints (a.k.a. “strict intervals”). The corresponding fact for the 1-topos Set Δ opSet^{\Delta^{op}} of simplicial sets is classical and due to Joyal (it’s described in “Sheaves in Geometry and Logic”), and the extension to (Gpd) Δ op(\infty Gpd)^{\Delta^{op}} is easy: the main thing to notice is that a flat functor from a 1-category to an (,1)(\infty,1)-category must land in the 0-truncated objects.

Thus, a basic property of the internal homotopy type theory of (Gpd) Δ op(\infty Gpd)^{\Delta^{op}} 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 (Gpd) Δ op(\infty Gpd)^{\Delta^{op}} itself. In particular, we could be in H Δ op\mathbf{H}^{\Delta^{op}} for any (,1)(\infty,1)-topos H\mathbf{H}, so that the theory applies to internal (infinity,1)-categories in any (,1)(\infty,1)-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 nn-simplex Δ n\Delta^n is the subtype of the nn-fold product I nI^n that consists of the ordered tuples (x 1x 2x n)(x_1 \le x_2 \le \dots\le x_n). 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 AA, the type of nn-simplices in AA is A nA Δ nA_n \coloneqq A^{\Delta^n}. In particular, the type of 11-simplices A 1A_1 in AA can also be called the type of morphisms in AA, while the type of 00-simplices A 0A_0 is equivalent to AA itself. We have a “source and target” map A 1A×AA_1 \to A \times A induced by precomposing with top and bot, and the (homotopy) fiber of this map over (a,b):A×A(a,b): A\times A can be called hom A(a,b)hom_A(a,b). Similarly, putting together a bunch of simplicial operators, we can inductively define the Segal maps segal A,n:A nA 1× A 0A 1× A 0× A 0A 1. segal_{A,n} \colon A_n \to A_1 \times_{A_0} A_1\times_{A_0} \dots \times_{A_0} A_1 . It’s then tempting to define AA to be a Segal type if these maps are equivalences, i.e. isSegal(A) n:isEquiv(segal A,n). isSegal(A) \coloneqq \prod_{n\colon \mathbb{N}} isEquiv(segal_{A,n}).

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 A nA_n is itself a simplicial space, not just a space, and so isSegal(A)isSegal(A) is asking a bunch of maps of simplicial spaces to be (levelwise) equivalences. The external space of 0-simplices of A nA_n is the external space of nn-simplices of AA, so if isSegal(A)isSegal(A) holds internally, that at least implies that AA is a Segal space externally.

In fact, I believe that in this case, isSegal(A)isSegal(A) says no more than that AA is an external Segal space. Being a Segal space is the same as being local with respect to some maps φ n:Δ 1+ Δ 0+ Δ 0Δ 1Δ n\varphi_n \colon \Delta^1 +_{\Delta^0} \cdots +_{\Delta^0} \Delta^1 \to \Delta^n, whereas isSegal(A)isSegal(A) should be asserting also locality with respect to φ n×Δ k\varphi_n \times \Delta^k for all kk. But Charles Rezk proved that if AA is a Segal space, then so is A KA^K for any simplicial space KK (that is, Segal spaces are an exponential ideal), and in particular so is A Δ kA^{\Delta^k}. Thus, this stronger property should follow automatically by adjointness.

Now in a Segal type, we can define composition hom A(b,c)×hom A(a,b)hom A(a,c) hom_A(b,c) \times hom_A(a,b) \to hom_A(a,c) in the usual way, by applying the inverse of segal A,2segal_{A,2} and then the diagonal operator A 2A 1A_2 \to A_1. We have an identity-assigning map AA 1A\to A_1 coming from degeneracies, and we can define what it means for an element f:hom A(a,b)f:hom_A(a,b) 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 ff 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 AA 1A\to A_1 factors through f:A 1isIntEquiv(f)\sum_{f\colon A_1} isIntEquiv(f). Thus, we can define a Segal type AA to be a Rezk type, or a category, if this map A f:A 1isIntEquiv(f)A\to \sum_{f\colon A_1} isIntEquiv(f) 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 Equiv A(a,b) f:hom A(a,b)isIntEquiv(f)Equiv_A(a,b) \coloneqq \sum_{f:hom_A(a,b)} isIntEquiv(f). Then path-elimination gives us an “internal path-to-equiv” morphism Id A(a,b)Equiv A(a,b)Id_A(a,b) \to Equiv_A(a,b), 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 (,1)(\infty,1)-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 \infty-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 (,n)(\infty,n)-categories, by working in the (,1)(\infty,1)-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 Θ\Theta, he proved that presheaves on Θ\Theta 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 (Gpd) Δ op(\infty Gpd)^{\Delta^{op}} that we might want to include as well. For instance, it is a cohesive (,1)(\infty,1)-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 A nA Δ nA_n \to A^{\partial \Delta^n} is an equivalence for all n1n\ge 1. This is of course equivalent to being local for the inclusions Δ nΔ n\partial\Delta^n \hookrightarrow \Delta^n. 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 \sharp) 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 BAB\to A we have (x:A)isCodiscrete(B(x))(x:A) \;\vdash\; isCodiscrete(B(x)) if and only if the square B B A A\array{ B & \to & \sharp B \\ \downarrow & &\downarrow \\ A & \to & \sharp A } is a pullback (as always in a cohesive topos). In this case, that means that the map BAB\to A of simplicial objects is uniquely determined (externally) by a map B 0A 0B_0 \to A_0 of non-simplicial objects.

The discrete objects are the constant ones: those where each simplicial operator A nA mA_n \to A_m 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 TypeType, 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.

  1. From the cohesive structure, we have the “type of codiscrete objects” CodiscType A:TypeisCodisc(A)CodiscType \coloneqq \sum_{A:Type} isCodisc(A). Since the codiscretes are left-exact reflective, this is itself codiscrete. It is also a full subtype of TypeType, i.e. maps to it by a (-1)-truncated morphism. Externally speaking, it is the \infty-groupoid of \infty-groupoids, regarded as a codiscrete simplicial \infty-groupoid (which is not the same as regarding it as an (,1)(\infty,1)-category and incarnating it as a Rezk type; remember that codiscrete simplicial objects are almost never Segal). Maps from AA into it classify “relatively codiscrete” maps BAB\to A as above.

  2. Any particular choice of a reflective subfibration that extends the discrete objects will also give us a full subtype of TypeType. Is there a choice for which we get something interesting here? What kind of maps BAB\to A are classified by this?

  3. 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 TypeType. Looking at small examples has suggested to me that if we make the obvious choice for Rezk types, we get a classifier for maps BAB\to A which are “Grothendieck constructions of morphisms into partial profunctors”. By this I mean that the fiber of BAB\to A over each 0-simplex of AA 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.

  4. We can also take various familiar (,1)(\infty,1)-categories, incarnate them as Rezk categories, and see what they look like internally. The most obvious choice is (,1)Cat(\infty,1)Cat itself, which should be a classifier for “Rezkian Cartesian opfibrations” (and similarly, (,1)Cat op(\infty,1)Cat^{op} 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”?

  5. Similarly, we have Gpd\infty Gpd and Gpd op\infty Gpd^{op}, incarnated as Rezk categories. I believe that Gpd op\infty Gpd^{op} will be a classifier for the sorts of fibrations that Charles mentions in his answer to this question, and of course Gpd\infty Gpd 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 00-truncated), but they still have to be handled explicitly in Coq. This leads to lots of extra paths and transports 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?

Posted at June 7, 2012 8:16 PM UTC

TrackBack URL for this Entry:   http://golem.ph.utexas.edu/cgi-bin/MT-3.0/dxy-tb.fcgi/2533

21 Comments & 1 Trackback

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 \infty-topos of simplicial objects. Something like this is what I tried to play around with (very unsuccessfully) in a recent nnForum 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”?

Posted by: Urs Schreiber on June 7, 2012 11:18 PM | Permalink | Reply to this

Re: Directed Homotopy Type Theory

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”?

I think that this would be classifier #5 (which I called Gpd\infty Gpd, referring to the “absolute” context). I don’t yet see any way to construct it, but there could well be one that I haven’t thought of.

If we knew how to define a “simplicial type”, then we could assert some axiom saying that any simplicial codiscrete type (semantically, a simplicial object in the underlying (,1)(\infty,1)-topos H\mathbf{H}) can be “realized” or “incarnated” as a single (non-codiscrete) type. A directed sort of geometric realization, perhaps constructed as an HIT. However, that brings us back to the problem of defining simplicial types.

Posted by: Mike Shulman on June 7, 2012 11:33 PM | Permalink | Reply to this

Re: Directed Homotopy Type Theory

I don’t yet see any way to construct it,

Ah, so when above in the post you say

Similarly, we have ∞Gpd and ∞Gpd op, incarnated as Rezk categories.

you mean that externally? Or are you talking at that point about something like

Grpd A:TypeisRezkGroupoid(A) \infty Grpd \coloneqq \sum_{A : Type} isRezkGroupoid(A)

?

Sorry, maybe I have lost you a bit towards the end of the entry.

One evident thing to look at in HoTT+[0-truncated strict interval] seems to be the “family” (not to say “simplicial type”) Type Type Δ Type_\bullet \coloneqq Type^{\Delta^\bullet}. That should be something like a simplicial incarnation of ProfProf, I assume?

Is TypeType a Segal type in HoTT+[0-truncated strict interval]? Is it a Rezk type? Can you see this, easily?

And just to be sure if I am correctly following: if AA is a Rezk type and XX is any type in HoTT+[0-truncated strict interval], then XAX \to A is a Rezk type, right?

Posted by: Urs Schreiber on June 8, 2012 3:12 PM | Permalink | Reply to this

Re: Directed Homotopy Type Theory

Prior to the numbered list, I said

Some of them we can construct from the directed interval, while others will probably have to be asserted axiomatically separately.

But I guess I wasn’t maximally explicit about which were which. I think #1–3 can be constructed; as far as I can tell #4–5 would have to be asserted axiomatically.

if A is a Rezk type and X is any type in HoTT+[0-truncated strict interval], then X→A is a Rezk type, right?

I think it should be, although I haven’t proven this yet. It would follow from identifying Rezk types with a localization, since any reflective subfibration is an exponential ideal.

Is TypeType a Segal type in HoTT+[0-truncated strict interval]?

No; look at what it classifies:

Type 0 =Gpd Δ op(Δ 0,Type)=Core(Gpd Δ op) Type 1 =Gpd Δ op(Δ 1,Type)=Core(Gpd Δ op/Δ 1) \begin{aligned} Type_0 &= \infty Gpd^{\Delta^{op}}(\Delta^0, Type) = Core(\infty Gpd^{\Delta^{op}})\\ Type_1 &= \infty Gpd^{\Delta^{op}}(\Delta^1, Type) = Core(\infty Gpd^{\Delta^{op}} / \Delta^1)\\ \dots \end{aligned}

There’s no unique way to glue two simplicial objects over Δ 1\Delta^1 to get a simplicial object over Δ 2\Delta^2, so the Segal condition fails.

I didn’t mention the classifier (,1)Prof(\infty,1)Prof, but I think it would fall somewhere between #3 and #4.

Posted by: Mike Shulman on June 8, 2012 5:18 PM | Permalink | Reply to this

Re: Directed Homotopy Type Theory

No; look at what it classifies:

Right, thanks.

I should find time to concentrate on this more. But it won’t happen at least before next week (since I am still at a workshop on something else…). So meanwhile I’ll just throw out more random questions, if you allow.

You wrote in the entry

Finally, there is an obvious way to generalize to (∞,n)-categories, by working in the (∞,1)-topos of cellular spaces rather than simplicial spaces, and mimicking Rezk’s Theta-spaces rather than complete Segal spaces.

Maybe even more obvious would be to generalize to (,n)(\infty,n)-categories by working in the (,1)(\infty,1)-topos of nn-fold simplicial \infty-groupoids and then mimicking Clark Barwick’s n-fold complete Segal spaces? Because: wouldn’t that simply amount, in your above setup, to asserting not the existence of a single, but of nn internal strict intervals?

That would also neatly fit with the “directed homotopy” picture. Instead of asserting just one notion of direction, we assert nn of them.

Posted by: Urs Schreiber on June 11, 2012 8:54 AM | Permalink | Reply to this

Re: Directed Homotopy Type Theory

wouldn’t that simply amount, in your above setup, to asserting not the existence of a single, but of nn internal strict intervals?

Well, I was attracted immediately to cellular sets because I knew that they are the classifying topos for something. Are you saying that nn-fold simplicial sets are the classifying topos for nn unrelated strict interval objects?

Posted by: Mike Shulman on June 11, 2012 10:46 PM | Permalink | Reply to this

Re: Directed Homotopy Type Theory

When I worked with directed spaces in the past, I had difficulties with simplices. It is difficult to build a sense of global causality in a space built from simplices. Instead, I fell back to “diamonds”, i.e. directed cubes.

This is a total naive question, but I wonder if things might work out better for you if you focus on cubes instead of simplices. For non-directed spaces, I don’t think it matters, but I think it does matter for directed spaces.

Posted by: Eric on June 8, 2012 1:09 AM | Permalink | Reply to this

Re: Directed Homotopy Type Theory

I think the difference is that you were starting with a predetermined notion of what a “directed space” should be and looking for a combinatorial model. Here, we are interested specifically in (,1)(\infty,1)-categories, which we already know have a well-behaved combinatorial model using simplices; only after the fact do we notice that simplicial spaces could be described internally as a sort of “directed spaces”. As I’ve been saying for a while, there’s no reason for there to be a unique correct notion of “directed space”.

It’s conceivable that (,1)(\infty,1)-categories can be modeled using cubes instead of simplices. However, that certainly wouldn’t solve the problem of formalization. And the other problems I discussed are just problems of our current ignorance, and our ignorance about cubical things is currently much greater than our ignorance about simplicial ones!

Posted by: Mike Shulman on June 8, 2012 4:58 PM | Permalink | Reply to this
Read the post Do Continental philosophers resent their lack of mathematical ability?
Weblog: Quora
Excerpt: Great answer, John! By the way, I would recommend those interested in the intersection of philosophy and mathematics to visit the n-category cafe: http://golem.ph.utexas.edu/category/ (John Baez is a contributor)
Tracked: June 8, 2012 5:48 PM

Re: Directed Homotopy Type Theory

Not that it’s worth much, but every time I hear about directed spaces, I think wistfully about forgetful (or obstructed) homotopies, and wonder if its time yet to hunt for a type theory in which dependent sum types come out as étale spaces rather than fibrations. Wistfully, because I’m quite sure of not being the right person to do the hunting.

Posted by: Jesse C. Mckeown on June 9, 2012 1:44 PM | Permalink | Reply to this

Re: Directed Homotopy Type Theory

When I was learning about the higher dimensional program from John Baez all those years ago, I took it that nn-categories were to be the basic entity. Then nn-groupoids were to be thought of a special case of nn-categories, particularly useful because homotopy theorists had worked out very powerful theories to deal with the former. The trick was to extend what they’d done, but to an environment with no inverses.

Do you think that what you’re finding here about the difficulty of directed homotopy type theory suggests that in some sense nn-groupoids shouldn’t be thought of as a variant of something more basic?

Perhaps there’s a lesson to be learned from why homotopy theory has flourished and why directed algebraic topology has been slow to develop and find the kind of range of applications throughout the rest of mathematics achieved by the non-directed version.

Also, back in the old days, John told us about an entity immediate between nn-groupoids and nn-categories, namely, nn-categories with duals. Do we expect a corresponding homotopy type theory for these? Given the work we did at the Café on the fundamental category of stratified spaces, perhaps we could looked for a stratified homotopy type theory.

(I wonder if every nn-category with duals is the fundamental category of some stratified space.)

I must say I had high hopes back here that something important was being said when John wrote

The basic idea is that nn-categories with duals describe the geometry of how things happen. When something drastic happens, we call it a catastrophe. So, catastrophe theory is related to nn-categories with duals.

I see I posed back to him

Now you might think there’s a good story here which goes: homotopy theorists have taught nn-category theorists a lot because they were already working on nn-groupoids, a special case of nn-category, without realising it. So now we find that those working on stratified spaces can teach us a lot because they are already working on a special case of nn-category (one with duals) without realising it.

I think that thread was the one I enjoyed most over the life of the Café.

Posted by: David Corfield on June 10, 2012 9:18 AM | Permalink | Reply to this

Re: Directed Homotopy Type Theory

I wondered

if every nn-category with duals is the fundamental category of some stratified space.

I see Woolf writes

Baez and Dolan’s insight is that transversal homotopy theory should associate categories with duals to stratified spaces just as homotopy theory associates groupoids to spaces… it is important to note that not every category with duals arises in this way; to obtain a correspondence one would require considerably more general objects on the geometric side.

Posted by: David Corfield on June 11, 2012 9:18 AM | Permalink | Reply to this

Re: Directed Homotopy Type Theory

David asks:

Do you think that what you’re finding here about the difficulty of directed homotopy type theory suggests that in some sense n-groupoids shouldn’t be thought of as a variant of something more basic?

Mike made some comments on how this question may or may not be an interesting open question in the first paragraphs of this post here. But notice that even if we adopt the point of view, as done here, that homotopy type theory, hence the notion of \infty-groupoids, is the fundamental notion, then \infty-groupoids nevertheless re-appear within this system as a special case of something more general:

in the ambient homotopy logic that already is about \infty-groupoids (with structure), there are the internal categories and their special case of internal groupoids, which externally are (sheaves of) (,1)(\infty,1)-categories and their special case of (sheaves of) \infty-groupoids.

Posted by: Urs Schreiber on June 11, 2012 9:21 AM | Permalink | Reply to this

Re: Directed Homotopy Type Theory

Do you think that what you’re finding here about the difficulty of directed homotopy type theory suggests that in some sense nn-groupoids shouldn’t be thought of as a variant of something more basic?

Yes, I think I would agree that it at least suggests it — as does the remarkable fruitfulness of homotopy theory that you mention. Another suggestive observation was recently re-raised on the categories mailing list: almost any sort of “structure” comes naturally with the correct notion of isomorphism or equivalence, but can admit many different kinds of morphism. For instance, nn-categories themselves admit not just ordinary functors, but ones which are lax and colax at many different levels, and similarly for transformations and higher transfors.

Also, not infrequently we are interested in higher-categorical structures other than nn-categories, such as nn-fold categories. And sometimes we are interested in Segal types that are not Rezk-complete, or which satisfy a modified version of Rezk-completeness: perhaps the best-known example is \dagger-categories, where the underlying groupoids contains only the unitary isomorphisms. But in all of these cases, there is an underlying nn-groupoid of objects.

All of this suggests that perhaps, we should regard nn-groupoids as a foundational notion, whereas nn-categories are specified structure on an underlying nn-groupoid of objects. Maybe.

Posted by: Mike Shulman on June 11, 2012 10:44 PM | Permalink | Reply to this

Re: Directed Homotopy Type Theory

Maybe.

It would mark quite a shift of ‘metaphysical’ viewpoint.

The idea of moving about the (n,r)(n, r)-categories table by processes such as homotopification and directification considers them on an equal foundational footing.

But now we can think of an overlay of activity (e.g., defining categories internally and their special cases, groupoids) on a foundation of \infty-groupoids. So there’s an initial homotopification, and then you go about your business, which might include some internal categorification, and indeed homotopification.

Perhaps the writing has been on the wall. As you mention, nn-categories are just one member of a zoo of similar constructions. Why single them out?

Time to rewrite those inspirational messages?

It is clear, therefore, that the set-based mathematics we know and love is just the tip of an immense iceberg of nn-categorical, and ultimately ω\omega-categorical, mathematics. (Categorification, p. 46)

becomes

It is clear, therefore, that the set-based mathematics we know and love is just the 0-truncated tip of an immense iceberg of nn-groupoidal, and ultimately \infty-groupoidal, mathematics, in which there are, among other things, a range of interesting higher category theoretic constructions.

Posted by: David Corfield on June 12, 2012 9:46 AM | Permalink | Reply to this

Re: Directed Homotopy Type Theory

Mike remarks:

First of all, there is lots of other structure on Grpd Δ op\infty Grpd^{\Delta^{op}} that we might want to include as well. For instance, it is a cohesive (∞,1)-topos.

By the way, in this perspective, a groupoid object X X_\bullet being effective implies in terms of cohesion that pieces have points in X X_\bullet.

Posted by: Urs Schreiber on June 11, 2012 9:38 AM | Permalink | Reply to this

Re: Directed Homotopy Type Theory

Very cool post. I’ve also been thinking recently about what directed type theory might look like, and more specifically, what it might look like if we try switching our shapes to the opetopes.

I talked about this at the recent meeting in Ljubljana, and I’ve put the slides online here in case anyone would like to have a look.

The main point, I guess, comes at the end where I show how the J-rule of type theory extends in a fairly natural way to “opetopic types” so that we can recover regular identity elimination by instantiating the generalized rule for the arrow (i.e. the unique 1-dimensional opetope.)

I think this might be a nice way to mix the idea of “making composition primitive” while at the same time preserving the nifty properties of J with regard to coherence. Of course, it’s still pretty speculative, but I thought it might be relevant to the discussion.

Posted by: Eric Finster on June 22, 2012 3:38 PM | Permalink | Reply to this

Re: Directed Homotopy Type Theory

Thanks for the link! This would be very neat, but I don’t understand it yet. I think I follow up until the page “Opetopic Formation and Introduction”. (Well, I didn’t try very hard to understand your bubble-tree notation, but I don’t think I should need it for understanding the type theory rules.)

I get the 𝒪\mathcal{O}-formation rule, but the 𝒪\mathcal{O}-composition rule confuses me. A niche contains less information than a frame, right? It’s missing the “target”. But the argument of Fill()Fill(-) is supposed to be a frame. What does N| τ(π)N|_{\tau(\pi)} mean and how is it a frame? I have a similar problem with the reflection rule; what does the notation \rhd mean? Maybe you explained all this in the talk…

Posted by: Mike Shulman on June 22, 2012 4:54 PM | Permalink | Reply to this

Re: Directed Homotopy Type Theory

Yes, sorry, slides are always a bit sparse.

The notation τ(π)\tau(\pi) means the target of my chosen opetope, which is an opetope of one dimension less. If I have chosen terms decorating the niche on π\pi then this means every face is decorated except the top dimensional one, and the top dimensional one in τ(π)\tau(\pi). Thus I have terms decorating the frame associated to τ(π)\tau(\pi) and this is what N| τ(π)N|_{\tau(\pi)} is supposed to represent: the decoration I get by restricting to the target. The composition lives in this filling type.

Since the first rule gives me a term in the filling type of this frame on τ(π)\tau(\pi), I can use that term to complete my nice NN on π\pi to a frame on π\pi. This is what the notation NcompN \triangleright comp means: it is my original niche extended to a frame by decorating the target cell with the composition obtained from the first rule.

Posted by: Eric Finster on June 22, 2012 6:01 PM | Permalink | Reply to this

Re: Directed Homotopy Type Theory

Ah, I see; thanks!

Let’s see, now on the next slide you say that when π\pi is a globe, there is a reduction rule comp(x)x\mathrm{comp}(x) \rightsquigarrow x. That seems weird to me, not least because it singles out globes. On the one hand, it seems like if this rule makes sense for globes, then it should also make sense whenever π\pi has only a single cell in its source. But on the other hand, why should we have any special cases? Shouldn’t the universality required of refl\mathrm{refl} automatically force comp(x)\mathrm{comp}(x) to be equivalent to xx in that case?

Now let’s see if I can understand your opetopic JJ-rule. You have a target type P(F,α)P(F,\alpha) which is allowed to depend on a filler α\alpha of a frame FF. And you suppose that this type is inhabited in the special case when the filler is the “refl” one specified by the 𝒪\mathcal{O}-composition and 𝒪\mathcal{O}-reflexivity rules. Then you conclude that for any frame GG and filler β\beta, the type P(G,β)P(G,\beta) is inhabited in a specified way.

Isn’t that going to force all of your cells to be “invertible” in some sense? The fillers for niches that are supposed to exist in an opetopic ω\omega-category are supposed to be special “universal” cells which exhibit their target as a “composite” of their source, but not every cell is universal in this way. So why should we expect to be able to say something about all cells based on a hypothesis only about these universal cells?

Posted by: Mike Shulman on June 22, 2012 6:45 PM | Permalink | Reply to this

Re: Directed Homotopy Type Theory

On the one hand, it seems like if this rule makes sense for globes, then it should also make sense whenever π\pi has only a single cell in its source.

Right. When talking about opetopes, I use the word “glob” in this more general sense. So I meant to include that case as well.

Shouldn’t the universality required of reflrefl automatically force comp(x)comp(x) to be equivalent to xx in that case?

I think so, yes. I guess I had in mind that in a type system, this notion of equivalence should have computational meaning, and hence that we would want the term xx and the term comp(x)comp(x) to have the same normal form. That’s why I mention the reduction rule.

What I would really like is to have a notion of “opetopic term” to complement the notion of “opetopic type.” When this is worked out, I will be able to say more about what this normal form might look like, and it may indeed be the case that there is nothing special about the reduction of globs.

Isn’t that going to force all of your cells to be invertible in some sense?

Yes, I think you are right about this. So perhaps this comment finds itself on the wrong page. :)

But nonetheless I think it’s useful to observe that the type theoretic rule corresponds nicely with the notion of universal filler. In a directed version, perhaps we can regard J as the definition of an opetopic ω\omega-groupoid.

Posted by: Eric Finster on June 23, 2012 11:11 AM | Permalink | Reply to this

Re: Directed Homotopy Type Theory

When talking about opetopes, I use the word “glob” in this more general sense.

Ah. I think that is fairly nonstandard; you might want to come up with a different word.

Thanks again for sharing your slides! Maybe one day I’ll get around to figuring out your strings-and-bubbles notation for opetopes. (-:

Posted by: Mike Shulman on June 23, 2012 6:00 PM | Permalink | Reply to this

Post a New Comment