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.

August 17, 2009

Chasing around the Triangle

Posted by David Corfield

While looking about for material for a new nnLab entry on foundations and philosophy, I came across Steve Awodey’s From Sets to Types to Categories to Sets. As the title of the paper suggests, Awodey chases around a triangle of foundational styles. In the process he demonstrates their equivalence.

The newest part of the triangle takes us from categories, in the form of toposes, to set theories. This involves the construction known as ‘ideal completion’ for categories (nnLab stub). Awodey explains how ideals are like classes, where principal ideals are the “sets”. The ideal completion of a topos is going to allow for the right kind of summing of types/sets into a universal object, into which there is a monomorphism from its own powerobject. Here powerobjects are formed by gathering subsets rather than subclasses.

After a fourth section which looks at the results of taking two steps around the triangle, the final section takes stock of what the whole exercise teaches us.

…the objects of type theory and set theory are structured by the operations of their respective systems in certain ways that are not mathematically salient. That additional information is essentially what is lost by our comparisons, e.g. distinctions between basic data and derived objects, between types of different complexity, ordinal rank of a set, membership chains within a set, etc. Categorical structure is closer to the mathematical content, and it is not lost in translation. Equivalence of categories preserves categorical properties and structures, because these are determined only up to isomorphism in the first place.

The structural approach implemented by category theory is thus more stable, more robust, more invariant than type or set theoretic constructions.

The latter two constructions are then likened to introducing coordinate systems on a manifold:

…no one today regards a manifold as involving specific coordinate charts, and one generally works with coordinate free methods so that the results obtained will apply directly – this is the modern, structural approach. But at times it can still be useful to introduce coordinates for some purpose, and this is unobjectionable, as long as the results are invariant. So it is with categorical versus logical foundations: category theory implements the structural approach directly. It admits interpretations of the conventional logical systems, without being tied to them. Category theory presents the invariant content of logical foundations.

But perhaps you’re wondering why category theory as a foundation should be restricted to toposes. What would happen if you looked to form an analogue triangle with (,1)(\infty, 1)-toposes in place of toposes as the category theoretic vertex of the triangle? Can we glimpse a parallel type theory and set theory? No doubt the former is related to other work by Steve on Homotopy theoretic models of identity types. And the set theory? Perhaps it ‘just’ needs ideal completion of a quasi-category.

Then a distant target of the parallel triangle for \infty-toposes presents itself.

Posted at August 17, 2009 11:39 AM UTC

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

14 Comments & 0 Trackbacks

Re: Chasing around the Triangle

If you think Steve Awodey’s paper on Homotopy theoretic models of identity types is cool, wait ‘til you see:

We are seeing the merging of homotopy theory and logic before our very eyes! I’ll say more about this in the next Week’s Finds.

Posted by: John Baez on August 17, 2009 4:33 PM | Permalink | Reply to this

Re: Chasing around the Triangle

Benno van den Berg and Richard Garner, Types are weak omega-groupoids.

Good to see this application!

I wanted to quickly add the link to the nnLab entry on Batanin ω\omega-categories – only to find that this still didn’t exist.

So I created a brief stub entry: Batanin ω\omega-category.

Hopefully somebody finds the time to say a bit more, maybe with an eye towards and motivated by this application to type theory.

Posted by: Urs Schreiber on August 17, 2009 8:05 PM | Permalink | Reply to this

Batanin ω-category

Is there a notion of simplicial nerve for Batanin ω\omega-categories?

Is the nerve of a Batanin ω\omega-groupoid a Kan coomplex?

Does every Kan complex, up to weak equivalence, arise this way?

Is this known?

I suppose it is. I am hoping somebody can reference page and verse and maybe even add it here (while I am busy with something else… ;-)

Posted by: Urs Schreiber on August 17, 2009 8:09 PM | Permalink | Reply to this

Re: Batanin ω-category

When I last checked, the best-developed notion of ‘nerve’ for Batanin’s globular ω\omega-categories was not a simplicial set but one of Joyal’s θ\theta-sets:

Maybe Michael or Denis-Charles can step in and tell us what people know today.

Posted by: John Baez on August 18, 2009 1:41 AM | Permalink | Reply to this

limits in Batanin ω-categories

When I last checked, the best-developed notion of ‘nerve’ for Batanin’s globular ω\omega-categories was not a simplicial set but one of Joyal’s θ\theta-sets:

Thanks!

One more:

is there a notion of limit in a Batanin ω\omega-category?

Or is there a notion of limit in a Joyal θ\theta-set, alternatively?

That should boil down to asking: is there a good way to say undercategory in Joyal ω\omega-categories / θ\theta-sets?

Surely there must be a simplicial nerve of a θ\theta-set, no?

Posted by: Urs Schreiber on August 18, 2009 7:36 AM | Permalink | Reply to this

Re: Batanin ω-category

I feel silly trying to guess answers to these questions given that Michael Batanin, Denis-Charles Cisinski, and other experts read this blog. Someone should wake them up.

Posted by: John Baez on August 18, 2009 9:05 PM | Permalink | Reply to this

Re: Chasing around the Triangle

It would be fun to guess the set analogue for the (,1)(\infty, 1) case. In the ordinary case, ideal completion of a topos gives something which is no longer a topos, but which contains a model of an elementary set theory (U, U)(U, \in_U). UU is the total ideal.

It looks like the topos SetSet gets sent to the category of classes of sets, containing the class of all sets, UU.

What could an ideal completion of a (,1)(\infty, 1)-topos such as TopTop look like – the completion under filtered colimits of monomorphisms? Do you get classes with a topology?

Posted by: David Corfield on August 20, 2009 10:54 AM | Permalink | Reply to this

classifiers in topos theory

I don’t know. I don’t even know about this in the ordinary case that you mention. But I have one general remark concerning this bit:

the completion under filtered colimits of monomorphisms?

I think it is an illusion of low categorical dimension that topos theory is fundamentally related to the notion of monomorphisms and subobjects.

This illusion arises because in the degenerate case of n=1n= -1, weak pullback of

* nCat \array{ {*} \\ \downarrow \\ n Cat }

happens to classify monomorphisms. But it is that map *nCat{*} \to n Cat which is fundamental, not the notion of monomorphism, and for higher nn there is no relation between the former and the latter.

For more on this see section 6.1.6 page 454 of HTT.

Posted by: Urs Schreiber on August 20, 2009 11:15 AM | Permalink | Reply to this

Re: classifiers in topos theory

The key thing would be to understand this ideal completion idea better. Awodey and Forssell write:

It is shown that a useful notion of ideal on a topos can be obtained by considering certain sheaves on the topos under the coherent (or finite epimorphic families) covering. Namely, these are those sheaves that occur as colimits of filtered diagrams of representables, in which every morphism is a monomorphism. Following a suggestion by André Joyal, these sheaves are characterized as satisfying a “small diagonal” condition with respect to maps with representable fibers. The subcategory of such ideals then forms a category with class structure in which one can solve for fixed points of the powerobject functor.

Posted by: David Corfield on August 20, 2009 11:44 AM | Permalink | Reply to this

Re: Chasing around the Triangle

I don’t think it’s quite right to say that the ideal completion of Set is “the” category of classes of sets. First of all, in order to make sense of the latter, you need to choose a more expressive set theory than ZFC, and different choices give you different results (even aside from the fact that any given first-order theory has lots of models). For instance, if you use von-Neumann-Bernays-Godel set-class theory, then the category of classes is not cartesian closed, whereas in some stronger set-class theories (such as Grothendieck universes with class := large set) it is. One can axiomatize what is meant by “a” category of classes containing Set (or any other given (pre)topos) as its category of sets, and any (material) set-class theory gives you an example. Now the ideal completion also gives you an example, but I don’t think it can naturally be identified with the one arising from any material set-class theory. In particular, by passing from the class of sets to the category of sets, you lose the ability to distinguish between isomorphic sets, so the ideal completion has to take place at a “structural” level rather than a “material” one. (See here for the meaning of “material” vs “structural”.)

Personally, I think that categories of classes are not really the most natural thing to consider. In most of mathematics, we never really treat about the elements of a proper class (such as the class of sets, or of groups) as elements of a set-like thing, but only as objects of some large category—in particular, we only think about them up to isomorphism. So rather than the category of classes, I think it is more interesting and illuminating to look at the 2-category of large categories. The analogue for an arbitrary topos is the 2-category of stacks on the topos, which has an internal logic and “contains the topos” as an object (via its self-indexing). This is quite close to the ideal completion, since as David quoted the latter can be defined using sheaves. In fact, the ideals living inside sheaves correspond fairly precisely to the “locally small” stacks living inside all stacks.

This suggests that the right analogue of ideal completion for an nn-topos is its (n+1)(n+1)-category of (locally small) nn-stacks, where of course nn could be \infty.

Posted by: Mike Shulman on August 30, 2009 4:21 AM | Permalink | Reply to this

Re: Chasing around the Triangle

Need to say that at the same time when Richard and Benno put their paper on arXiv also Peter Lumsdaine from CMU proved the same result (his paper appeared on arXiv just one day later). It’s nice to compare those papers as Richard’s and Benno’s proof is rather ‘category-theoretical’
while Peter’s is purely proof-theoretical.

Together with Joachim Kock from Universitat Autonoma de Barcelona, I led a seminar on Peter’s proof and found it comprehensible also for people not working in logic and type theory.

Posted by: Chris Kapulkin on August 31, 2009 3:50 PM | Permalink | Reply to this

Re: Chasing around the Triangle

By the way, it’s interesting to note that this triangle really doesn’t depend at all on the use of proper classes or large categories. The passage from (material) sets to types by giving set-theoretic semantics doesn’t use them, nor does the passage from types to categories by constructing a syntactic category. The passage back from categories to types via the internal logic also evidently requires no proper classes, so the only subtlety is in the passage from categories to (material) sets.

If you insist on constructing, from a given (pre)topos, a model of material set theory in the internal language of some category, then you need that category to be a “category of classes” and you need something like the ideal construction. But if you only want a model of a first-order material set theory, on an even footing with the model of the first-order theory of elementary toposes (aka structural set theory) that you started with*, then it suffices to define a “set” to be an isomorphism class of objects of the topos equipped with extensional well-founded relations. (If you don’t care about the axiom of foundation, then it suffices to consider merely extensional relations.) You can then define the “\in” relation between such things and prove the axioms of material set theory. This construction dates back to J.C. Cole in the 1970s and can also be found in Peter Johnstone’s original book Topos Theory.

So what is a well-founded object in an nn-category?

(* Of course, those both might be living in the internal logic of some ambient category, but they don’t have to be.)

Posted by: Mike Shulman on August 30, 2009 4:36 AM | Permalink | Reply to this

Re: Chasing around the Triangle

This is done on the Lab at [[pure set]].

Posted by: Toby Bartels on August 30, 2009 7:39 AM | Permalink | Reply to this

Re: Chasing around the Triangle

Actually, I misspoke; what I said is only strictly true if you consider well-pointed topoi (such as ETCS). For a general topos you do end up in an internal language (that of the topos).

Posted by: Mike Shulman on August 31, 2009 4:10 AM | Permalink | Reply to this

Post a New Comment