The n-Category Café

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 $(\infty,1)$-category $(\infty Gpd)^{\Delta^{op}}$ of simplicial $\infty$-groupoids is, itself, an $(\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 $(\infty Gpd)^{\Delta^{op}}$, as a place to talk about $(\infty,1)$-categories (incarnated as Rezk categories).

Of course, for this to work, we’ll need to make some of the special structure of $(\infty Gpd)^{\Delta^{op}}$ visible in its internal homotopy type theory. The most important observation is that $(\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^{\Delta^{op}}$ of simplicial sets is classical and due to Joyal (it’s described in “Sheaves in Geometry and Logic”), and the extension to $(\infty Gpd)^{\Delta^{op}}$ is easy: the main thing to notice is that a flat functor from a 1-category to an $(\infty,1)$-category must land in the 0-truncated objects.

Thus, a basic property of the internal homotopy type theory of $(\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 $(\infty Gpd)^{\Delta^{op}}$ itself. In particular, we could be in $\mathbf{H}^{\Delta^{op}}$ for any $(\infty,1)$-topos $\mathbf{H}$, so that the theory applies to internal (infinity,1)-categories in any $(\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 $n$-simplex $\Delta^n$ is the subtype of the $n$-fold product $I^n$ that consists of the ordered tuples $(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 $A$, the type of $n$-simplices in $A$ is $A_n \coloneqq A^{\Delta^n}$. In particular, the type of $1$-simplices $A_1$ in $A$ can also be called the type of morphisms in $A$, while the type of $0$-simplices $A_0$ is equivalent to $A$ itself. We have a “source and target” map $A_1 \to A \times A$ induced by precomposing with top and bot, and the (homotopy) fiber of this map over $(a,b): A\times A$ can be called $hom_A(a,b)$. Similarly, putting together a bunch of simplicial operators, we can inductively define the Segal maps $$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 $A$ to be a Segal type if these maps are equivalences, i.e. $$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_n$ is itself a simplicial space, not just a space, and so $isSegal(A)$ is asking a bunch of maps of simplicial spaces to be (levelwise) equivalences. The external space of 0-simplices of $A_n$ is the external space of $n$-simplices of $A$, so if $isSegal(A)$ holds internally, that at least implies that $A$ is a Segal space externally.

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

Now in a Segal type, we can define composition $$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,2}$ and then the diagonal operator $A_2 \to A_1$. We have an identity-assigning map $A\to A_1$ coming from degeneracies, and we can define what it means for an element $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 $f$ 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 $A\to A_1$ factors through $\sum_{f\colon A_1} isIntEquiv(f)$. Thus, we can define a Segal type $A$ to be a Rezk type, or a category, if this map $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) \coloneqq \sum_{f:hom_A(a,b)} isIntEquiv(f)$. Then path-elimination gives us an “internal path-to-equiv” morphism $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 $(\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 $(\infty,n)$-categories, by working in the $(\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 $(\infty Gpd)^{\Delta^{op}}$ that we might want to include as well. For instance, it is a cohesive $(\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_n \to A^{\partial \Delta^n}$ is an equivalence for all $n\ge 1$. This is of course equivalent to being local for the inclusions $\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 $B\to A$ we have $(x:A) \;\vdash\; isCodiscrete(B(x))$ if and only if the square $$\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 $B\to A$ of simplicial objects is uniquely determined (externally) by a map $B_0 \to A_0$ of non-simplicial objects.

The discrete objects are the constant ones: those where each simplicial operator $A_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 $Type$, 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 \coloneqq \sum_{A:Type} isCodisc(A)$. Since the codiscretes are left-exact reflective, this is itself codiscrete. It is also a full subtype of $Type$, 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 $(\infty,1)$-category and incarnating it as a Rezk type; remember that codiscrete simplicial objects are almost never Segal). Maps from $A$ into it classify “relatively codiscrete” maps $B\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 $Type$. Is there a choice for which we get something interesting here? What kind of maps $B\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 $Type$. Looking at small examples has suggested to me that if we make the obvious choice for Rezk types, we get a classifier for maps $B\to A$ which are “Grothendieck constructions of morphisms into partial profunctors”. By this I mean that the fiber of $B\to A$ over each 0-simplex of $A$ 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 $(\infty,1)$-categories, incarnate them as Rezk categories, and see what they look like internally. The most obvious choice is $(\infty,1)Cat$ itself, which should be a classifier for “Rezkian Cartesian opfibrations” (and similarly, $(\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 $\infty Gpd$ and $\infty Gpd^{op}$, incarnated as Rezk categories. I believe that $\infty Gpd^{op}$ will be a classifier for the sorts of fibrations that Charles mentions in his answer to this question, and of course $\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 $0$-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?