The n-Category Café

I expect everyone would agree that these are all reasonable axioms to impose. The first three are together a simple categorification of one of the equivalent definitions of elementary 1-topos: a locally cartesian closed category with finite limits and colimits and a subobject classifier. In the 1-categorical case we can get away with less: we can construct local cartesian closure and finite colimits from ordinary cartesian closure and the subobject classifier. This seems less likely to be true in the $\infty$-case, but if it is, then it would be just a simplification of the above definition, not a modification of it.

The fourth axiom is a more contentful categorification of a subobject classifier. The most natural categorification would be a classifier for all objects, i.e. a morphism $p:V\to U$ such that pullback of $p$ yields an equvialence from $Hom(X,U)$ to the core of the slice over $X$. But this is inconsistent due to Cantorian size paradoxes, so the existence of “sufficiently many” object classifiers closed under the other categorical structure is a suitable replacement. Note that we don’t assume given a specific “tower” of universes each contained in the next, but we can nevertheless construct “enlargements” as necessary: for any object classifier $p:V\to U$, we can find an object classifier classifying $p+! : V+U \to U+1$ to obtain a “universe” $U'$ such that both “$U\subseteq U'$” and “$U\in U'$”. (That this works depends on the disjointness of coproducts, which follows from the above definition in the same way that disjointness of coproducts follows for an elementary 1-topos; see this nlab page about the definition.)

It’s reasonably well-known that any Grothendieck $(\infty,1)$-topos satisfies all of these axioms, at least if there exist arbitrarily large inaccessible cardinals (a Grothendieck $(\infty,1)$-topos has an object classifiers for the relatively $\kappa$-compact morphisms, for any regular cardinal $\kappa$, but we need $\kappa$ to be inaccessible in order for this class of morphisms to be closed under dependent products as well). Moreover, all of these axioms correspond (at least, intuitively/conjecturally) to well-known type formers in homotopy type theory: finite limits give $\Sigma$-types, identity types, a unit type, and finite product types; finite colimits give non-recursive higher inductive types (including coproduct types and an empty type); local cartesian closure gives $\Pi$-types satisfying function extensionality; a subobject classifier gives an impredicative type of all propositions (i.e. with the axiom that the HoTT Book calls “propositional resizing”, plus the appropriate propositional form of univalence); and the object classifiers give universes satisfying the univalence axiom.

The real question is, are these axioms sufficient for something to merit the name “elementary $(\infty,1)$-topos”? This is where I’ve recently had a change of heart. I used to believe that we also ought to include categorical structure corresponding to recursive higher inductive types as well, and that therefore the definition of “elementary $(\infty,1)$-topos” would have to wait for an agreed-upon and sufficiently general definition of exactly what a “higher inductive type” is. But now, although I still think that’s an important question, I don’t think it’s directly relevant to the definition of elementary $(\infty,1)$-topos.

There are a couple of reasons for this. One is that not even every elementary 1-topos admits arbitrary higher inductive types (though it does have all ordinary inductive types). For with higher inductive types we can show that any (even infinitary) algebraic theory has an initial model (essentially, write down the operations and axioms as inductive generators), whereas this is not the case in all elementary 1-toposes. Andreas Blass’s paper Words, free algebras, and coequalizers shows that (assuming the consistency of arbitrarily large compact cardinals) the axioms of ZF set theory (without the axiom of choice) cannot prove that all algebraic theories have initial models. The idea is to write down an algebraic theory whose initial model would have to be an uncountable regular cardinal, which (by a result of Gitik) cannot be proven to exist in ZF. Thus, there are models of ZF which, regarded as elementary 1-toposes, do not admit all higher inductive types.

I think it’s not unreasonable to consider this a defect of the notion of elementary 1-topos. However, the latter definition is so entrenched that it seems folly to try to change it; rather we ought, if we are interested in it, to define a stronger notion of “elementary 1-topos with higher inductive types”. Moreover, there’s also a virtue to the simplicity of the definition of elementary 1-topos; the stronger notion will probably be rather more complicated. By analogy, then, we ought not to demand all higher inductives of an elementary $(\infty,1)$-topos. This has the additional advantage of allowing us to proceed with the theory of elementary $(\infty,1)$-topoi now, rather than blocking on a general definition of higher inductive types.

So much for arbitrary recursive higher inductives. But there are a few inductive or higher-inductive constructions, at least, that we certainly don’t want to do without, such as:

• The natural numbers (which allow us to construct the integers, rationals, and real numbers as well). Although not included in the definition of elementary 1-topos, a natural numbers object (NNO) often has to be added to the hypotheses of theorems about them. In the $(\infty,1)$-case it’s even harder to do without. For instance, a basic theorem of synthetic homotopy theory like $\Omega S^1 = \mathbb{Z}$ requires the natural numbers in order to construct $\mathbb{Z}$ (though see below). The infinity in $(\infty,1)$ also often requires the natural numbers, such as when proving things about $n$-types by induction (although we could consider an “external” induction instead).

• Relatedly, the $n$-truncation operation of type theory, which in category theory corresponds to the (n-truncated, n-connected) factorization system. Synthetic homotopy theory, in particular, requires truncations in many places. We could simply assume the existence of truncations, but I’ve always felt uncomfortable with that, because once we start “adding things just because we want them”, how do we know where to stop? Should we include more HITs? All of them?

The second reason I’m now willing to propose a precise definition of elementary $(\infty,1)$-topos is that we now know (well, mostly; see below) that these two constructions exist automatically. That is, from the definition I gave above of elementary $(\infty,1)$-topos, we can construct a NNO and an ($n$-truncated, $n$-connected) factorization system. Therefore, we can stop at that definition, which is nice and simple and clearly analogous to an elementary 1-topos, and yet have all the necessary basic structure with which to do synthetic homotopy theory.

The construction of $n$-truncation is due to Egbert Rijke, and proceeds by induction on $n$. The $(-1)$-truncation can be defined impredicatively using the subobject classifier: in type theory it is $\Vert A \Vert = \prod_{P:Prop} (A\to P) \to P$, the smallest proposition implied by $A$. In category theory, the $(-1)$-image of $f:A\to B$ is the internally-smallest subobject of $B$ through which $f$ factors, and is likewise constructed using the subobject classifier. Now if we have the $n$-truncation $\Vert A \Vert_n$, we define $\Vert A \Vert_{n+1}$ to be the $(-1)$-image of the map $A \to U^A$, whose transpose $A\times A \to U$ classifies the $n$-image of the diagonal $A\to A\times A$, for some universe $U$ that classifies this map. In type theory, this is $\sum_{H:A\to Type} \Vert \sum_{x:A} \prod_{y:A} H(y) = \Vert x=y\Vert_n \Vert$.

As stated, this construction “goes up a universe level” at each step. In category theory, where we don’t have a fixed tower of universes, what this means is that it doesn’t allow us to assert the existence of object classifiers that are closed under the $n$-truncation (for $n\gt -1$). However, Egbert also showed (see his paper The join construction) that with a NNO this can be remedied: if $A$ belongs to a universe $U$ (is “small”) and $B$ is “locally small” in the sense that its diagonal $B\to B\times B$ is classified by $U$ (i.e. its identity types are all in $U$), then any map $A\to B$ has a $(-1)$-image that is also $U$-small, constructed as a sequential colimit of joins. This allows us to construct inductively (and, with a NNO, internally inductively rather than externally) the sequence of $n$-truncations lying in the same universe.

Thus, if we have an NNO, then we have $n$-truncations. But we can also construct an NNO, in the following way. Note that a universe that is closed under finite limits and colimits is necessarily “infinite”, for it contains all the finite types $1+1+\cdots+1$. An NNO is, by definition, the “smallest infinite set” in a certain precise sense, so it makes sense that with a subobject classifier we can construct it once we have any infinite object. We can certainly find the smallest sub-type of $U$ containing $0$ and closed under coproducts with $1$. This is not 0-truncated, by univalence, since finite sets have automorphisms; but we can remedy this by imposing rigid structure on our finite types. (Steve Awodey has pointed out that this is closely related to Frege’s definition of the natural numbers.) I formalized such an argument here using graphs, but posets or something else would probably work as well. I also expect that a similar argument should work for all W-types (i.e. non-higher inductive types), following roughly the known proof that W-types exist in any elementary 1-topos with an NNO.

Note that both constructions are currently written in type theory, so formally speaking their applicability to elementary $(\infty,1)$-toposes depends on the still-conjectural intepretation of type theory in the latter. However, I have complete faith that both could also be manually translated into category-theoretic language.

Despite all this, I do regard the above definition as tentative: it’s a concrete proposal, but still just a proposal. If you can think of anything wrong with it, or anything missing, I’m very open to hearing about it. I also want to mention a fow of open questions that are important even if this definition is correct:

• Is every groupoid object in an elementary $(\infty,1)$-topos necessarily effective? Since this is part of the natural generalization of the Giraud exactness axioms to the $\infty$-case, it’s very tempting to include it as part of the definition of elementary $(\infty,1)$-topos; but I don’t consider that permissible since a groupoid object is infinitary, and an “elementary” $(\infty,1)$-topos should involve only finitary axioms.

• What elementary $(\infty,1)$-toposes are there, other than Grothendieck ones? Because universes have to be infinite, we can’t have an $\infty$-analogue of finitary toposes like $FinSet$. We can impose other cardinality bounds — for instance, if the inaccessible cardinals are unbounded below some cardinal $\lambda$, then the category of $\infty$-groupoids of cardinality below $\lambda$ should be an elementary $(\infty,1)$-topos. And for formal reasons, the $(\infty,1)$-category of elementary $(\infty,1)$-toposes (equipped with a chosen tower of object classifiers preserved by the “logical functors”) should have an initial object, which conjecturally ought to be presented syntactically by homotopy type theory.

  A more interesting question is whether there are $\infty$-analogues of constructions on elementary 1-toposes that don’t preserve Grothendieck-ness, such as filterquotients, gluing, uniformly continuous actions of topological groups, actions of large groupoids, and so on. I suspect so, but it would be worth someone writing out the details. (Various homotopy type theorists are currently working, from different perspectives, on $\infty$-notions of realizability topos.)

• Rather than constructing an NNO from a universe, a different approach that occurs to many people is to use $\Omega S^1$. If we have a NNO, then we can prove that $\Omega S^1 = \mathbb{Z}$, so it’s reasonable to hope that even without an assumed NNO we could show that $\Omega S^1$ has some properties of $\mathbb{Z}$ and construct the natural numbers from it. Egbert and I haven’t yet been able to figure out a way to do this. However, I at least can’t claim to have thought about it for more than a few hours, so there may still be a relatively easy solution.

  Such a construction of $\mathbb{N}$ would certainly be more satisfying. Moreover, it would apply to any “$(\infty,1)$-$\Pi$-pretopos”, which I would be inclined to define as a locally cartesian closed $(\infty,1)$-category with finite limits and finite colimits satisfying “descent” (which follows from the existence of object classifiers). Type-theoretically, descent means that although we don’t assume any universes, our non-recursive higher inductives have a “large elimination principle” inspired by univalence, in which path-constructors correspond directly to equivalences.