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.

April 4, 2017

Elementary (∞,1)-Topoi

Posted by Mike Shulman

Toposes come in two varieties: “Grothendieck” and “elementary”. A Grothendieck topos is the category of sheaves of sets on some site. An elementary topos is a cartesian closed category with finite limits and a subobject classifier. Though these definitions seem quite different, they are very closely related: every Grothendieck topos is an elementary topos, while elementary toposes (especially when considered “over a fixed base”) behave very much like Grothendieck ones.

All the fervor about (,1)(\infty,1)-toposes nowadays has centered on Grothendieck ones: (,1)(\infty,1)-categories of \infty-sheaves of \infty-groupoids on (,1)(\infty,1)-sites. (Technically, this is only true if we use a perhaps-excessively-general notion of “site”, but it’s the right idea.) However, it’s quite natural to speculate about a corresponding notion of elementary (,1)(\infty,1)-topos. Because an elementary 1-topos is essentially “a category whose internal logic is intuitionistic higher-order type theory”, it’s natural to try to define an elementary (,1)(\infty,1)-topos to be an (,1)(\infty,1)-category whose “internal logic” is, or at least should be, a kind of homotopy type theory. However, even laying aside the unresolved questions involved in the “internal logic” of (,1)(\infty,1)-categories, it’s never been entirely clear to me exactly what “kind” of homotopy type theory we should use here.

Until now, that is. I propose the following definition: an elementary (∞,1)-topos is an (,1)(\infty,1)-category such that

  • It has finite limits and colimits (in the \infty-sense, i.e. homotopy limits and colimits).
  • It is locally cartesian closed.
  • It has a subobject classifier, i.e. a map :1Ω\top:1\to \Omega such that for any XX the hom-\infty-groupoid Hom(X,Ω)Hom(X,\Omega) is equivalent, by pullback of \top, to the \infty-groupoid of subobjects of XX (which is equivalent to a discrete set). Here a “subobject” is a map SXS\to X such that each \infty-functor Hom(Z,S)Hom(Z,X)Hom(Z,S) \to Hom(Z,X) is fully faithful.
  • For any morphism f:YXf:Y\to X, there exists an object classifier p:VUp:V\to U that classifies ff (i.e. ff is a pullback of pp) and such that the collection of morphisms it classifies (i.e. the pullbacks of pp) is closed under composition, finite fiberwise limits and colimits, and dependent products. Here p:VUp:V\to U is an “object classifier” if for any XX, pullback of pp yields a fully faithful functor from Hom(X,U)Hom(X,U) to the core (the maximal sub-\infty-groupoid) of the slice (,1)(\infty,1)-category over XX.

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:VUp:V\to U such that pullback of pp yields an equvialence from Hom(X,U)Hom(X,U) to the core of the slice over XX. 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:VUp:V\to U, we can find an object classifier classifying p+!:V+UU+1p+! : V+U \to U+1 to obtain a “universe” UU' such that both “UUU\subseteq U'” and “UUU\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 (,1)(\infty,1)-topos satisfies all of these axioms, at least if there exist arbitrarily large inaccessible cardinals (a Grothendieck (,1)(\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 (,1)(\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 (,1)(\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 (,1)(\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 (,1)(\infty,1)-topos. This has the additional advantage of allowing us to proceed with the theory of elementary (,1)(\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 (,1)(\infty,1)-case it’s even harder to do without. For instance, a basic theorem of synthetic homotopy theory like ΩS 1=\Omega S^1 = \mathbb{Z} requires the natural numbers in order to construct \mathbb{Z} (though see below). The infinity in (,1)(\infty,1) also often requires the natural numbers, such as when proving things about nn-types by induction (although we could consider an “external” induction instead).

  • Relatedly, the nn-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 (,1)(\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 (,1)(\infty,1)-topos, we can construct a NNO and an (nn-truncated, nn-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 nn-truncation is due to Egbert Rijke, and proceeds by induction on nn. The (1)(-1)-truncation can be defined impredicatively using the subobject classifier: in type theory it is A= P:Prop(AP)P\Vert A \Vert = \prod_{P:Prop} (A\to P) \to P, the smallest proposition implied by AA. In category theory, the (1)(-1)-image of f:ABf:A\to B is the internally-smallest subobject of BB through which ff factors, and is likewise constructed using the subobject classifier. Now if we have the nn-truncation A n\Vert A \Vert_n, we define A n+1\Vert A \Vert_{n+1} to be the (1)(-1)-image of the map AU AA \to U^A, whose transpose A×AUA\times A \to U classifies the nn-image of the diagonal AA×AA\to A\times A, for some universe UU that classifies this map. In type theory, this is H:AType x:A y:AH(y)=x=y n\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 nn-truncation (for n>1n\gt -1). However, Egbert also showed (see his paper The join construction) that with a NNO this can be remedied: if AA belongs to a universe UU (is “small”) and BB is “locally small” in the sense that its diagonal BB×BB\to B\times B is classified by UU (i.e. its identity types are all in UU), then any map ABA\to B has a (1)(-1)-image that is also UU-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 nn-truncations lying in the same universe.

Thus, if we have an NNO, then we have nn-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++11+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 UU containing 00 and closed under coproducts with 11. 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 (,1)(\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 (,1)(\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 (,1)(\infty,1)-topos; but I don’t consider that permissible since a groupoid object is infinitary, and an “elementary” (,1)(\infty,1)-topos should involve only finitary axioms.

  • What elementary (,1)(\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 FinSetFinSet. 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 (,1)(\infty,1)-topos. And for formal reasons, the (,1)(\infty,1)-category of elementary (,1)(\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 ΩS 1\Omega S^1. If we have a NNO, then we can prove that ΩS 1=\Omega S^1 = \mathbb{Z}, so it’s reasonable to hope that even without an assumed NNO we could show that ΩS 1\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 “(,1)(\infty,1)-Π\Pi-pretopos”, which I would be inclined to define as a locally cartesian closed (,1)(\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.

Posted at April 4, 2017 9:08 AM UTC

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

17 Comments & 0 Trackbacks

Re: Elementary (∞,1)-Topoi

We can do a fair amount of category theory inside an elementary 1-topos (for instance, we can develop Grothendieck 1-topos theory relative to this base). I would expect that for a reasonable definition of elementary (,1)(\infty,1)-topos, we should likewise be able to do some (,1)(\infty,1)-category theory, but we don’t yet know how (or even whether it’s posstible) to do that with your definition, right?

Posted by: Ulrik Buchholtz on April 4, 2017 12:56 PM | Permalink | Reply to this

Re: Elementary (∞,1)-Topoi

Wellll… it depends on how “internal” you want to be. It’s true that we don’t (yet) know how to define (,1)(\infty,1)-categories in type theory, which translates to saying that we don’t know how to construct a universe of internal (,1)(\infty,1)-categories in an elementary (,1)(\infty,1)-topos (by this definition). However, speaking externally about an elementary (,1)(\infty,1)-topos, we can define the notion of an internal (,1)(\infty,1)-category in it, and likewise internal presheaves on such and so on. Without arbitrary HITs we may not be able to construct localizations at arbitrary sets of maps, but insofar as such localizations do exist, I would expect that we ought to be able to study relatively-Grothendieck (,1)(\infty,1)-toposes.

I do admit that this is a defect of the proposed definition, however.

Posted by: Mike Shulman on April 4, 2017 6:23 PM | Permalink | Reply to this

Re: Elementary (∞,1)-Topoi

Although, without countable (co)limits it isn’t clear how to construct left/right Kan extensions for such internal (,1)(\infty,1)-categories, which might get in the way of a theory of relatively-Grothendieck (,1)(\infty,1)-toposes.

Posted by: Mike Shulman on April 4, 2017 7:49 PM | Permalink | Reply to this

Re: Elementary (∞,1)-Topoi

The first question that comes to my mind is whether this will be stable under some localizations. It would be nice if the category of motivic spaces would be an elementary​ infinity-topos, to get something like a motivic homotopy type theory, to prove interesting theorems in a synthetic way.

Would that localization (of the infinity topos of simplicial Nisnevich homotopy sheaves, say) be still elementary? Or is there a known obstruction?

Posted by: Konrad Voelkel on April 4, 2017 6:54 PM | Permalink | Reply to this

Re: Elementary (∞,1)-Topoi

Well, I don’t know what motivic spaces are. I would expect that any accessible left exact localization of an elementary (,1)(\infty,1)-topos is again such (and, of course, Grothendieck if we started with a Grothendieck one), but for non-left-exact localizations I wouldn’t expect it to be true. Non-left-exact localizations don’t generally preserve the exactness properties of toposes.

Posted by: Mike Shulman on April 4, 2017 7:51 PM | Permalink | Reply to this

Re: Elementary (∞,1)-Topoi

So I’m wondering if it’s inevitable for an elementary (∞,1)-topos to be so strong. In type-theoretic terms, you have the subobject classifier as an element of the other universes. This makes them “Grothendieck-sized”. What if we could make them smaller?

Maybe, instead of having a type like “Prop”, and Martin-Löf’s countable universe hierarchy, we have a “Uv” type constructor and a “Pow” type constructor. Uv has an associated “El” coercion, to give universes. Pow(T) has a coercion to T->Uv(…), for some desired Uv. The Uvs are not closed under Pow. Extra stuff to give Pows propositional truncations of Uv-based type families. There is no large elimination per-se, so these type constructors don’t give you any V_ω-sized types. Do you see the sort of thing I’m thinking of?

I haven’t written anything down, so it might totally not work, but my intuition is that you could get HOL-strength (∞,1)-topoi this way.

I guess a possible objection is that a classical interpretation of function types wouldn’t actually fit in these Uvs, unless they’re effectively closed under Pow after all.

Maybe Uvs don’t need to be closed under function types. The “type” judgment is, and we can get a Uv around a given type, in order to use univalence.

Posted by: Matt Oliveri on April 4, 2017 11:08 PM | Permalink | Reply to this

Re: Elementary (∞,1)-Topoi

I don’t know what you mean, can you describe it in category-theoretic terms?

Posted by: Mike Shulman on April 5, 2017 12:17 AM | Permalink | Reply to this

Re: Elementary (∞,1)-Topoi

Hmm. So my syntax idea was flawed, I now realize. So you aren’t missing much there. The gist of the idea, if I understand this sort of categorical definition, is to remove or weaken the requirement that the object classifiers be closed under dependent function type formation.

The aspect of the syntax I still think I got right is to use a “Uv” type constructor to guarantee enough object classifiers, rather than the usual countable hierarchy of constant universes, like in book HoTT.

Posted by: Matt Oliveri on April 5, 2017 6:02 AM | Permalink | Reply to this

Re: Elementary (∞,1)-Topoi

I’m a little doubtful that such object classifiers would be very useful, though I haven’t actually checked how often we use the closure of universes under Π\Pi.

Posted by: Mike Shulman on April 5, 2017 12:55 PM | Permalink | Reply to this

Re: Elementary (∞,1)-Topoi

It seems that you are rejecting the analogy

Toposes : Inductive Types :: (oo,1)-Toposes : HITs.

Could you say why that is?

Posted by: Colin Zwanziger on April 5, 2017 6:35 AM | Permalink | Reply to this

Re: Elementary (∞,1)-Topoi

Categorically, ordinary inductive types are about being able to construct free monads on (polynomial) endofunctors, while higher inductive types are roughly about being able to construct presented monads by taking colimits of such free monads. The basic non-recursive inductive type is a coproduct; the basic non-recursive higher inductive type is a pushout or coequalizer. This dichotomy is essentially indepedent of categorical dimension: a 1-topos can have inductive types or it can have higher inductive types, and similarly for an (,1)(\infty,1)-topos. And as I mentioned in the post, a general elementary 1-topos doesn’t have all higher inductive types, so it seems reasonable not to require the same for an (,1)(\infty,1)-topos either.

Posted by: Mike Shulman on April 5, 2017 1:00 PM | Permalink | Reply to this

Re: Elementary (∞,1)-Topoi

Under your proposed definition, is every slice of an elementary (,1)(\infty, 1)-topos an elementary (,1)(\infty, 1)-topos?

(Of course, I mean “slice” in the (,1)(\infty, 1)-sense.)

I believe Peter Freyd called the analogous result for elementary 1-toposes the “fundamental theorem of topos theory”, though I don’t know the justification for such a grand name.

Posted by: Tom Leinster on April 5, 2017 10:31 AM | Permalink | Reply to this

Re: Elementary (∞,1)-Topoi

Good question! The answer is yes. Finite limits and colimits are inherited by slice (,1)(\infty,1)-categories, just as in the 1-categorical case: colimits in a slice category are just colimits in the base, while limits in a slice category are limits of a diagram extended with the base object (so products become pullbacks, etc.). Moreover, because “a slice of a slice is a slice”, (/X)/(f:YX)/Y(\mathcal{E}/X)/(f:Y\to X) \simeq \mathcal{E}/Y, local cartesian closure is inherited by slice categories, and the pullback of any (sub)object classifier to a slice category is a (sub)object classifier therein. (Indeed, by asking for local cartesian closure as part of the definition, I’ve made this theorem rather more trivial than in the 1-categorical case.)

Posted by: Mike Shulman on April 5, 2017 1:07 PM | Permalink | Reply to this

Re: Elementary (∞,1)-Topoi

What can one say about the (,1)(\infty, 1)-parallel to Lambek and Scott’s discussion of the free topos in Introduction to higher order categorical logic? (See also nLab: free topos.)

Example 16.1 they have the free topos as generated by ‘pure type theory’. Does something similar happen with a ‘pure HoTT’?

On p. 127 they see the construction of the free topos as reconciling intuitionism, Platonism and formalism. A step too far?

Posted by: David Corfield on April 6, 2017 10:01 AM | Permalink | Reply to this

Re: Elementary (∞,1)-Topoi

Looking over your post again, I’m asking for more on this comment:

And for formal reasons, the (,1)(\infty,1)-category of elementary (,1)(\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.

Is this the kind of ‘moral’ should and ought, where if it doesn’t work out, something needs fixing to make it work out?

Posted by: David Corfield on April 6, 2017 10:14 AM | Permalink | Reply to this

Re: Elementary (∞,1)-Topoi

Is this the kind of ‘moral’ should and ought, where if it doesn’t work out, something needs fixing to make it work out?

Probably. Although it’s always good to admit the possibility that things might fail to work out in a way that shows our expectations were wrong in the first place.

they see the construction of the free topos as reconciling intuitionism, Platonism and formalism. A step too far?

In my opinion, yes. The free topos is a mathematical object, so it “exists” in the same sense that any other mathematical object “exists”. So I don’t see how it could do anything to reconcile differing philosophical positions about the meaning of mathematical existence.

Posted by: Mike Shulman on April 6, 2017 8:06 PM | Permalink | Reply to this

Re: Elementary (∞,1)-Topoi

I wrote:

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.

It seems that Rech and Schäfer are already working on coding up such a construction here.

Posted by: Mike Shulman on July 8, 2017 5:23 PM | Permalink | Reply to this

Post a New Comment