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.

October 18, 2012

Object Classifiers and (∞,1)-Quasitoposes

Posted by Mike Shulman

I’m spending this year at the Institute for Advanced Study in Princeton with a bunch of homotopy type theorists and fans. So far things have been mostly ramping up slowly, but there’s significant progress already being made in a few areas (mainly technical ones), and indications of more exciting things down the line. I intend to have some posts soon about what we’ve been up to, but first I want to advertise this recent preprint:

Although the title refers to Voevodsky’s univalence axiom for homotopy type theory, the paper is primarily about the (,1)(\infty,1)-categorical structure that models it, namely object classifiers.

An object classifier in an (n,1)(n,1)-category H\mathbf{H} is an object UU such that for any XX, the hom-groupoid H(X,U)\mathbf{H}(X,U) is naturally equivalent to (a small full subgroupoid of) the groupoid of objects over XX, Core(H/X)Core(\mathbf{H}/X). However, since H\mathbf{H} is an (n,1)(n,1)-category, its hom-category H(X,U)\mathbf{H}(X,U) is an (n1,1)(n-1,1)-category, and so the collection of objects over XX classified by maps into UU must be a sub-(n1,1)(n-1,1)-category of the (n,1)(n,1)-category H/X\mathbf{H}/X. The obvious way to make this work is to take it to consist of (n2)(n-2)-truncated objects. For instance, in the classical case when H\mathbf{H} is a 1-category, we can only expect to classify a sub-poset of H/X\mathbf{H}/X, and the standard poset to classify is that of subobjects of XX (i.e. (1)(-1)-truncated objects of H/X\mathbf{H}/X) — we then get the standard topos-theoretic notion of a subobject classifier.

However, because 1=\infty-1=\infty, when H\mathbf{H} is an (,1)(\infty,1)-category it can contain classifiers for objects with no “truncation” restriction being necessary. To a topologist, object classifiers are familiar under the name of classifying spaces: for any FF, the classifying space BAut(F)\mathbf{B}Aut(F) is an object classifier for the subgroupoid of H/X\mathbf{H}/X consisting of the spaces over XX all of whose fibers are FF. On the other hand, any (,1)(\infty,1)-topos contains an object classifier for all “κ\kappa-compact objects”, for any sufficiently large cardinal κ\kappa. (The size restriction is necessary to avoid Cantorian paradoxes.)

This latter property basically characterizes (,1)(\infty,1)-topos among locally presentable (,1)(\infty,1)-categories. However, one can ask whether (,1)(\infty,1)-categories that aren’t (,1)(\infty,1)-toposes can contain classifiers for other classes of objects. Gepner and Kock give a positive answer to this question, using an elegant categorification of the Garner-Lack theory of Grothendieck quasitoposes.

A Grothendieck (1-)topos is the category of sheaves on some site. A Grothendieck quasitopos is the category of separated presheaves on some site. Grothendieck quasitoposes have many of the properties of toposes: they are locally cartesian closed, complete and cocomplete, and locally presentable, but instead of a subobject classifier they have only a “strong-subobject classifier”: this is like a subobject classifier but it classifies only strong monomorphisms.

Thus, when in search of more exotic object classifiers, it is natural to look for a notion of (,1)(\infty,1)-quasitopos. This, in turn, requires categorifying the notion of “separated presheaf”. Gepner and Kock start from the characterization that a presheaf XSet C opX\in Set^{C^{op}} is separated if and only if XLXX \to L X is a monomorphism in Set C opSet^{C^{op}}, where LL is the (left exact) reflection of Set C opSet^{C^{op}} into the subcategory of sheaves. This definition is convenient because every (,1)(\infty,1)-topos is a left-exact reflective subcategory of an (,1)(\infty,1)-presheaf category, but we don’t yet have a sufficiently general notion of “site” to be able to characterize all (,1)(\infty,1)-toposes as consisting of “sheaves”.

However, categorifying this definition does require choosing a way to categorify the notion of “monomorphism”, for which there are multiple choices. Rather than fixing a particular choice, Gepner and Kock show that it doesn’t matter: you can use any stable factorization system which is preserved by the reflector. Thus we arrive at their

Definition: Let P\mathbf{P} be an (,1)(\infty,1)-topos, (,)(\mathcal{E},\mathcal{M}) a stable factorization system on P\mathbf{P}, and L:PPL:\mathbf{P}\to \mathbf{P} a left exact reflector which preserves (,)(\mathcal{E},\mathcal{M}). An object XPX\in \mathbf{P} is \mathcal{M}-separated if XLXX\to L X is in \mathcal{M}. An (,1)(\infty,1)-quasitopos is an (,1)(\infty,1)-category consisting of the \mathcal{M}-separated objects in such a situation.

In particular, if we were to interpret this definition in 1-category theory, we would get something apparently more general than the usual notion of (Grothendieck) quasitopos. (We would get the usual notion if we fixed (,)(\mathcal{E},\mathcal{M}) to be (epi, mono).) It would be interesting to see how much of the theory of 1-quasitoposes carries over to these more general “quasitoposes relative to a factorization system”, and also how much of it extends to the \infty-case.

In particular, any category of concrete (∞,1)-sheaves is an (,1)(\infty,1)-quasitopos. Motivated by these, there is an nLab page called (∞,1)-quasitoposes; this gives a definition which is clearly closely related to Gepner and Kock’s definition, but is not identical. I think that the nLab definition is precisely the special case of Gepner and Kock’s definition where

  1. P\mathbf{P} is the (,1)(\infty,1)-topos of (,1)(\infty,1)-sheaves on some (,1)(\infty,1)-site (C,J)(C,J),
  2. (,)(\mathcal{E},\mathcal{M}) is the (nn-connected, nn-truncated) factorization system for some nn, and
  3. LL is the reflector corresponding to a different, larger topology KK on the same category CC.

On reflection, I think Gepner and Kock’s choice to use an arbitrary left-exact reflector LL is preferable, since not every (,1)(\infty,1)-topos consists of sheaves. In particular, their definition includes all (,1)(\infty,1)-toposes as (,1)(\infty,1)-quasitoposes, which seems like a desirable feature. It’s less obvious to me whether one wants to allow any stable factorization system (rather than just the (connected, truncated) ones). Quite possibly one does (and I’m very fond of stable factorization systems myself), but the theory of (,1)(\infty,1)-quasitoposes is currently so embryonic that I’d like to see more theory to justify one choice or the other.

One bit of theory justifying Gepner and Kock’s choice is that they get object classifiers at their level of generality. How? Well, in 1-category theory, every quasitopos contains a topos. In a presentation as the separated presheaves, this topos consists of the sheaves. Its objects can also be characterized internally in the quasitopos as the “coarse” ones (those that are orthogonal to all monic epis). The first description works just as well (,1)(\infty,1)-categorically: every object of the reflective subcategory corresponding to LL is \mathcal{M}-separated, since \mathcal{M} contains the equivalences, and these objects form an (,1)(\infty,1)-topos. I don’t know whether they have an internal characterization in this case.

Anyway, the upshot is that any object classifier in the (,1)(\infty,1)-topos of coarse objects is also an object classifier in the whole (,1)(\infty,1)-quasitopos. The morphisms it classifies will always be “fiberwise coarse”; in particular, plenty of objects will not be classified by any of the object classifiers obtained in this way. Gepner and Kock write

Presumably there should be a direct characterization of this … class in terms of some notion of strong map, depending on the factorization system… just as in the classical case [it] consists of strong monos.

Sounds probably related to the question of finding an internal characterization of the coarse objects.

In addition to posing good questions like these for future research, there’s more good stuff in Gepner and Kock’s paper. They construct an object classifier in an nn-topos which classifies some (n1)(n-1)-truncated objects (as opposed to the (n2)(n-2)-truncated ones that one would naively expect to have to require). They also construct one in motivic homotopy theory (which I know absolutely nothing about). And they give another proof (the first proof by Denis-Charles Cisinski was here on this blog) that every locally presentable, locally cartesian closed (,1)(\infty,1)-category can be presented by a right proper Cisinski model category.

This last fact is, with current technology, central to our ability to actually model type theory in (,1)(\infty,1)-categories (i.e. to deal with the strictness/coherence issues). We still don’t have a general solution for this which includes (univalent) universes, although I’ve recently heard some rumors that there may be something along those lines forthcoming soon. (Of course, like all rumors, they could be exaggerated…)

Posted at October 18, 2012 1:35 AM UTC

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

15 Comments & 1 Trackback

Re: Object Classifiers and (∞,1)-Quasitoposes

A basic question: what is the meaning of the H\mathbf{H} that appears in the first line after the fold?

Posted by: Tom Leinster on October 24, 2012 12:20 PM | Permalink | Reply to this

Re: Object Classifiers and (∞,1)-Quasitoposes

It’s an nn-category.

Posted by: Mike Shulman on October 24, 2012 12:34 PM | Permalink | Reply to this

Re: Object Classifiers and (∞,1)-Quasitoposes

Really? So how is H(X,U)\mathbf{H}(X, U) a groupoid? As you say in the second sentence after the fold, if H\mathbf{H} is an nn-category then H(X,U)\mathbf{H}(X, U) is an (n1)(n - 1)-category.

Posted by: Tom Leinster on October 24, 2012 1:10 PM | Permalink | Reply to this

Re: Object Classifiers and (∞,1)-Quasitoposes

Oops, thanks for catching that. I was trying to be more general than necessary in one place without being correspondingly general elsewhere. Let’s restrict to (n,1)(n,1)-categories to be sure of making sense; everything gets more complicated when you have noninvertible 2-cells, and the main subject is the (,1)(\infty,1)-case. I’ve edited the post.

Posted by: Mike Shulman on October 24, 2012 2:11 PM | Permalink | Reply to this

Re: Object Classifiers and (∞,1)-Quasitoposes

Allow me to play devil’s advocate for a moment. To quote from the abstract,

“It follows that every \infty-topos has a hierarchy of “universal” univalent families, indexed by regular cardinals…”

What if there aren’t many regular cardinals? Of course, we have to break the axiom of choice very badly to end up in that situation, and even though univalent foundations is in some sense the ultimately intuitionistic approach (internal logic of an (,1)(\infty,1)-category and all…), I feel that somehow AC is used in the metalanguage to some extent - at least in looking at models using sSetsSet etc.

Posted by: David Roberts on October 24, 2012 2:37 PM | Permalink | Reply to this

Re: Object Classifiers and (∞,1)-Quasitoposes

Well, on the one hand, HoTT itself can be fully constructive, including its metalanguage (which might be something like a ‘logical framework’). But on the other hand, it has set-theoretic models in higher (quasi)toposes, whose construction does indeed make serious use of choice, excluded middle, and inaccessible cardinals.

It’s an important open question whether one can construct set-theoretic models of HoTT when the ambient set theory is itself constructive. I think in the long run, an even more important question will be whether starting from HoTT itself, in its full constructivity, we can construct new models of HoTT in internally defined higher (quasi)toposes — that way we could use HoTT as a real foundation for mathematics and still reap the benefits of internalization. So you have a good point that we can’t yet do everything we’d like to be able to do constructively with HoTT, even though the theory itself is constructive: there’s lots of work still to be done!

Posted by: Mike Shulman on October 24, 2012 10:53 PM | Permalink | Reply to this

Re: Object Classifiers and (∞,1)-Quasitoposes

Dear Mike, could you be more specific about the use of inaccessible cardinals? I don’t see where we really need more then classical ZFC to produce set-theoretic models of HoTT in terms of higher categories. For instance, the proof of the univalence axiom in the model of simplicial sets can be (in fact, is) done within ZFC, so that I don’t understand where inaccessible cardinals show up as a necessity.

Posted by: Denis-Charles Cisinski on October 25, 2012 1:03 AM | Permalink | Reply to this

Re: Object Classifiers and (∞,1)-Quasitoposes

We need the collection of kan fibrations that are classified by the univalent one to be closed under all the type forming operations, including dependent sums and dependent products. It seems to me that closure under dependent sums requires the cardinal bound to be regular, and closure under dependent products requires it to be a strong limit.

Posted by: Mike Shulman on October 25, 2012 1:51 AM | Permalink | Reply to this

Re: Object Classifiers and (∞,1)-Quasitoposes

Can’t we be a little more careful? I mean, we can look at Kan fibrations with α\alpha-small fibers for a regular cardinal α\alpha. These will be closed under type forming operations involving strictly less than α\alpha data. Working with the univalent fibration p αp_\alpha which classifies Kan fibrations with α\alpha-small fibers will be enough if we let α\alpha vary to follow our needs, or won’t it? This would involve a proof that our final results do not depend on the choices of α\alpha we made (locally in ur constructions and proofs), but, we have the same issue if we work with universes.

Posted by: Denis-Charles Cisinski on October 25, 2012 2:15 AM | Permalink | Reply to this

Re: Object Classifiers and (∞,1)-Quasitoposes

Sounds plausible, but I don’t have any objections to inaccessibles, and it’s simpler to just have one universe.

Posted by: Mike Shulman on October 25, 2012 2:46 AM | Permalink | Reply to this

Re: Object Classifiers and (∞,1)-Quasitoposes

I don’t have objections to inaccessibles. It is just that controling sizes consists to control “constructibility” in some sense (which is specified by the cardinals we use or not), so that I have the habit to take care of this. And I would really be interested to meet a mathematical situation where inaccessible cardinals necessarily show up while we did not specifically ask for them (it seems that inaccessible cardinals are often used for the comodity of the exposition, not for their real meaning, which consists to ensure the existence of some objects which we could not reach otherwise). In fact, speaking of comodity of the exposition, can’t we expect type theory to deal with the logical distinctions between different kind of smallness, without the necessity to specify if we work with Grothendieck universes or not? (I realize that this really is not the purpose of your nice post, and I don’t mean to bother you with all this, so please answer only if you enjoy it!)

Posted by: Denis-Charles Cisinski on October 25, 2012 8:49 PM | Permalink | Reply to this

Re: Object Classifiers and (∞,1)-Quasitoposes

I don’t mind the discussion, but I don’t quite understand what you’re after. Type theory does explicitly posit universes, so it’s not as if the need for universes comes out of nowhere without our asking for them. What do you mean by “logical distinctions between different kinds of smallness”?

Posted by: Mike Shulman on October 25, 2012 9:26 PM | Permalink | Reply to this

Re: Object Classifiers and (∞,1)-Quasitoposes

I did not realize that type theory posit universes (my bad). Nevertheless, the principles type theory is after (expressing mathematics in a certain way) do not require universes, and we could still discuss why a theory with the purpose of type theory should require universes, except fot the comodity of exposition (we could work with a sequence of regular cardinals to express various notions of smallness, for instance). In some sense, we may all agree by really speaking category-theoretically (instead of set-theoretically): we work with an (elementary) topos which you think of as the category of sets, you have a bunch of full subcategories which are also topoi (and whose objects are the “small sets”), and you don’t care if such things where constructed set-theoretically using regular or inaccessible cardinals. As for the “logical distinction etc”, that was ill posed. However, here is another question which is related to all this: how does the presence of universes manifests itself in programming languages (such as coq)? Are they necessary there?

Posted by: Denis-Charles Cisinski on October 26, 2012 1:22 AM | Permalink | Reply to this

Re: Object Classifiers and (∞,1)-Quasitoposes

I should probably clarify that not all type theories have universes. However, the univalence axiom can only be stated in a type theory that has universes. (There are certain weaker consequences of univalence that can be stated as slightly more arbitrary-looking rules in some type theories without universes, but the simplest statement of univalence requires a universe to be univalent.)

Maybe a type theorist could say more about what “principles” type theory is “after” and how they relate to universes. (I do believe that universes were first introduced by Martin-Lof in some of his earliest work on type theory.) Personally, I’m interested in (homotopy) type theory because it offers a higher-categorical foundation for mathematics, and in particular for (higher) category theory, and also for internalization into higher categories. And it’s very convenient to have universes of small sets in order to say things like the Yoneda lemma. There are various tricks in a set-theoretic world that you can do to pretend you have universes without really having them (e.g. Feferman set theory), which work more or less well, and I don’t have trouble believing that similar sorts of things might work in some type theories, or especially in set-theoretic modeling of type theory. But currently I feel that in the language we actually speak when doing mathematics, we want to come as close as we possibly can to having a type of all types.

When doing mathematics in Coq, universes are needed for the same sorts of things that one needs them for in other kinds of mathematics. And specifically when doing homotopy type theory, we use them a lot for the univalence axiom (so much so that we’re currently leaning on the Coq developers to implement better universe polymorphism). But I doubt that universes were used very much for the odd-order theorem, just as they probably aren’t used much in the informal mathematical proof of that (although I don’t actually know anything about it). And similarly, when writing verified computer code in Coq such as Compcert, I doubt that universes play much of a role.

Posted by: Mike Shulman on October 26, 2012 1:36 AM | Permalink | Reply to this

Re: Object Classifiers and (∞,1)-Quasitoposes

Just in case anyone is interested, it is possible to force the nonexistence of any inaccessibles and keep AC by forcing “ORDORD is not Mahlo” and then doing some Easton forcing. I learned this from Joel Hamkins’ latest.

Posted by: David Roberts on October 26, 2012 6:31 AM | Permalink | Reply to this
Read the post Freedom From Logic
Weblog: The n-Category Café
Excerpt: Towards a way of doing homotopy type theory informally, and a new opinion regarding propositions as types.
Tracked: November 10, 2012 2:56 AM

Post a New Comment