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.

March 10, 2017

The Logic of Space

Posted by Mike Shulman

Mathieu Anel and Gabriel Catren are editing a book called New Spaces for Mathematics and Physics, about all different kinds of notions of “space” and their applications. Among other things, there are chapters about smooth spaces, \infty-groupoids, topos theory, stacks, and various other things of interest to nn-Cafe patrons, all of which I am looking forward to reading. There are chapters by our own John Baez about the continuum and Urs Schreiber about higher prequantum geometry. Here is my own contribution:

I intend this to be my last effort at popularization of HoTT for some time, and accordingly it ended up being rather comprehensive. It begins with a 20-page introduction to type theory, from the perspective of a mathematician wanting to use it as an internal language for categories. There are many introductions to type theory, but probably not enough from this point of view, and moreover most popularizations of type theory are rather vague about its categorical semantics; thus I chose (with some additional prompting from the editors) to spend quite some time on this, and be fairly (though not completely) precise about exactly how the categorical semantics of type theory works.

I also decided to emphasize the point of view that type theory (and “syntax” more generally) is a presentation of the initial object in some category of structured categories. Some category theorists respond to this by saying essentially “what good is it to describe that initial object in some complicated way, rather than just studying it categorically?” It’s taken me a while to be able to express the answer in a really satisfying way (at least, one that satisfies me), and I tried to do so here. The short version is that by explicitly constructing an object that has some universal property, we may learn more about it than we can conclude from the mere statement of its universal property. This is one of the reasons that topologists study classifying spaces, category theorists study classifying toposes, and algebraists study free groups. For a longer answer, read the chapter.

After this introduction to ordinary type theory, but before moving on to homotopy type theory, I spent a while on synthetic topology: type theory treated as an internal language for a category of spaces (actual space-spaces, not \infty-groupoids). This seemed appropriate since the book is about all different kinds of space. It also provides a good justification of type theory’s constructive logic for a classical mathematician, since classical principles like the law of excluded middle and the axiom of choice are simply false in categories of spaces (e.g. a continuous surjection generally fails to have a continuous section).

I also introduced some specific toposes of spaces, such as Johnstone’s topological topos and the toposes of continuous sets and smooth sets. I also mentioned their “local” or “cohesive” nature, and how it can be regarded as explaining why so many objects in mathematics come “naturally” with topological structure. Namely, because mathematics can be done in type theory, and thereby interpreted in any topos, any mathematical construction can be interpreted in a topos of spaces; and since the forgetful functor from a local/cohesive topos preserves most categorical operations, in most cases the “underlying set” of such an interpretation is what we would get by performing the same construction directly with sets. This also tell us in what circumstances we should expect a construction that takes account of topology to disagree with its analogue for discrete sets, and in what circumstances we should expect a set-theoretic construction to inherit a nontrivial topology even when there is no topological input; read the chapter for details.

The subsequent introduction to homotopy type theory and synthetic homotopy theory has nothing particularly special about it, although I decided to downplay the role of “fibration categories” in favor of (,1)(\infty,1)-categories when talking about higher-categorical semantics. Current technology for constructing higher-categorical interpretations of type theory uses fibration categories, but I don’t regard that as necessarily essential, and future technology may move away from it. In particular, in addition to the intuition of identity types as path objects in a model category, I think it’s valuable to have a similar intution for identity types as diagonal morphisms in an (,1)(\infty,1)-category.

The last section brings everything together by discussing cohesive homotopy type theory, which is of course one of my current personal interests, modeling the local/cohesive structure of an (,1)(\infty,1)-topos with modalities inside homotopy type theory. As I’ve said before, I feel that this perspective greatly clarifies the distinction and relationship between space-spaces and \infty-groupoid “spaces”, with the connecting “fundamental \infty-groupoid” functor characterized by a simple universal property.

Finally, in the conclusion I at last allowed myself some philosophical rein to speculate about synthetic theories as foundations for mathematics, as opposed to simply internal languages for categories constructed in an ambient classical mathematics. Once we see that mathematics can be formulated in type theory to apply equally well in a category of spaces as in the category of sets, there is no particular reason to regard the category of sets as the “true” foundation and the category of spaces as “less foundational”. Just as we can construct a category of spaces from a category of sets by equipping sets with topological structure, we can construct a “category of sets” (i.e. a Boolean topos) from a “category of spaces” by restricting to the subcategory of objects with uninteresting topology (the discrete or codiscrete ones). Either category, therefore, can serve as an equally valid “reference frame” from which to describe mathematics.

Posted at March 10, 2017 12:58 PM UTC

TrackBack URL for this Entry:

15 Comments & 0 Trackbacks

Re: The Logic of Space

I presume reign is a typo for rein?

Posted by: Gavin Wraith on March 10, 2017 3:43 PM | Permalink | Reply to this

Re: The Logic of Space

Yes, thanks, fixed.

Posted by: Mike Shulman on March 10, 2017 4:35 PM | Permalink | Reply to this

Re: The Logic of Space

Just as the quasitopos of subsequential spaces sits inside the topos of subsequential spaces

Is this a typo?

Posted by: David Roberts on March 11, 2017 1:34 AM | Permalink | Reply to this

Re: The Logic of Space

Bah, yes. The second “subsequential” should be “consequential”.

Posted by: Mike Shulman on March 11, 2017 3:52 AM | Permalink | Reply to this

Re: The Logic of Space

Very much enjoying this article, probably the clearest description I’ve ever read of the categorical semantics of type theory.

Could you say a bit more about what is meant by footnote 32 about the product being given by a “mapping out” property? Is it because the product is “baked in” as the structure of the context itself?

Posted by: Max S. New on March 11, 2017 4:19 AM | Permalink | Reply to this

Re: The Logic of Space

I’m glad you like it!

Is it because the product is “baked in” as the structure of the context itself?

That’s one way of thinking about it: in the usual way of describing the semantics of type theory the category has to have finite products simply to interpret all the contexts, whether or not the type theory has product types. However, as I said in the footnote, a better way to say it is that semantics of type theory naturally occurs in a cartesian multicategory, and in a cartesian multicategory finite products coincide with the “tensor products” of a “representable multicategory”, which have a mapping-out universal property. I guess you could also describe that as having the product “baked into” the structure of the context: the definition of cartesian multicategory is written just so as to “virtualize” the notion of category with finite products, just as an ordinary multicategory “virtualizes” the notion of monoidal category.

Posted by: Mike Shulman on March 11, 2017 4:48 PM | Permalink | Reply to this

Re: The Logic of Space

I know you refer to Hamkins’ article –The set-theoretic multiverse – in a footnote, but perhaps a comparison of your pluralist view with his ‘mulitverse view’ would illuminate the discussion.

You say

in ZFC orthodoxy there is an absolute notion of “set” out of which everything is constructed.

This agrees with Hamkins’ ‘universe view’:

The universe view is the commonly held philosophical position that there is a unique absolute background concept of set, instantiated in the corresponding absolute set-theoretic universe, the cumulative universe of all sets, in which every set-theoretic assertion has a definite truth value.

He departs from this:

I shall argue for a contrary position, the multiverse view, which holds that there are diverse distinct concepts of set, each instantiated in a corresponding set-theoretic universe, which exhibit diverse set-theoretic truths. Each such universe exists independently in the same Platonic sense that proponents of the universe view regard their universe to exist.

I take it that your pluralism is more radical still to allow for a much wider range of synthetic theories:

…from a pluralistic viewpoint, mathematics can be developed relative to any topos, obeying the same general rules of type theory.

(Presumably this is using the convention of dropping the \infty from \infty-topos.)

Are you counting Hamkins’ multiverse as a small corner of your “multitude of universes of mathematics”, or were you pointing to varieties of type theory/topos?

Posted by: David Corfield on March 12, 2017 10:49 AM | Permalink | Reply to this

Re: The Logic of Space

Informally, I would certainly count ZFC-universes as “universes of mathematics”. Formally, I don’t think I can give a definition of a “universe of mathematics” that includes both models of ZFC as well as toposes. But since ZFC includes strong axioms like foundation, replacement, and choice, its models are determined uniquely by their corresponding topos of sets. (Though this is no longer quite true for weaker membership-based set theories.) Such toposes are of course a very restricted class, being Boolean and satisfying the axiom of choice, but on the other hand those axioms can be dropped from ZFC without trouble; I don’t recall Hamkins’ attitude towards constructive logic, but in principle a constructive set theorist could believe in a universe or a multiverse in the same way.

Probably the more significant departure is that Hamkins’ universes instantiate different “concepts of set”, whereas the pluralistic viewpoint I would advocate for is that the foundation of mathematics doesn’t need to be sets at all, but could equally well be “spaces” or something else.

Posted by: Mike Shulman on March 13, 2017 4:46 PM | Permalink | Reply to this

Re: The Logic of Space

Someone might wonder how the two cosmological analogies - multiverse/universes and reference frames - are to fit together, or is this asking too much of analogies? There are some exotic cosmological notions of multiple universes on offer, e.g., here.

Perhaps the largest issue for you is the access one universe may or may not have to another. For Hamkins,

… we do not expect to see the whole multiverse from within any particular universe. Nevertheless, set theory does have a remarkable ability to refer internally to many alternative set concepts, as when we consider definable inner models or various outer models to which we have access.

Posted by: David Corfield on March 15, 2017 9:49 AM | Permalink | Reply to this

Re: The Logic of Space

The fact that from one foundational model we can construct and discuss many others is one reason that I think the “reference frames” analogy is better than the “universes” one. But even that isn’t an exact analogy, since from any reference frame we can always transition to any other one — and in particular, converting from frame 1 to frame 2 is always reversible — whereas if we start from one topos like SetSet and then internalize in some other topos EE, we may not be able to get back to SetSet in any obvious way. For instance, if EE has no global points, then we can’t regard SetSet as an EE-topos. I suppose maybe someone could try to stretch the analogy to consider “reference frames” like the inside of the event horizon of a black hole, but that seems a bit dubious.

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

Re: The Logic of Space

Perhaps your totality of frames/universes is more readily formed bicategorically than a bicategory for the set-multiverse.

Posted by: David Corfield on March 16, 2017 3:05 PM | Permalink | Reply to this

Re: The Logic of Space

Certainly; bicategories of topoi are well-studied. But it’s still not as simple as one might think, for instance because there are at least two kinds of morphism between toposes: geometric and logical.

Posted by: Mike Shulman on March 16, 2017 4:48 PM | Permalink | Reply to this

Re: The Logic of Space

So once you’ve settled on the definition of elementary (infinity, 1)-topos, and so know what a logical functor is there, we’ll have (,2)(\infty, 2)-equivalents of the three bicategories at Topos: Topos\mathbf{Topos}, GrTopos\mathbf{GrTopos}, and LogTopos\mathbf{Log Topos}.

Posted by: David Corfield on March 16, 2017 5:19 PM | Permalink | Reply to this

Re: The Logic of Space

Minor language nit on page 58: “and also more novel synthetic mathematics using of nonclassical structure”. I think either plain “using” or “making use of” would read more idiomatically.

Posted by: Blake Stacey on March 19, 2017 11:58 PM | Permalink | Reply to this

Re: The Logic of Space

Thanks, will fix the typo.

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

Post a New Comment