Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
1 to 13 of 13
Has anyone thought about exponentiability for -toposes? I think the Johnstone-Joyal paper “Continuous categories and exponentiable toposes” is crying out to be categorified – there’s even a 1-truncated hypercover in it!
I’ve dropped a reference to the following paper at continuous category:
I’ve also started a new page exponentiable topos to drop some references there.
Whenever I see results like this, I think to myself: what if we just take as axiomatic that any result from ordinary category theory can be lifted to -category theory?! It is pretty clear that this principle is valid, so why not just ignore the technicalities and a) focus on showing what can be done with such a lift, b) focus on defining once and for all a general mechanism for formulating and carrying out this lift?
Thanks! I added some cross-links to the “Examples” section of exponentiable object and at continuous category.
Re #3: Actually the principle is false; consider for instance the statement that every diagonal map is a monomorphism. It should be possible to isolate a class of statements for which it does hold, but this requires formulating a suitably general context (either syntactic or semantic) for “formal category theory”, which is work in progress.
Hehe, yes, this was deliberately a bit blasé :-), but the essence of it is I think valid. I completely agree regarding your second statement. Do you know of any work in a syntactic direction on this (I am aware of the semantic work of Riehl and Verity, though I’m not sure it goes/is intended to go quite as far as I have in mind)?
Do you count Riehl-Shulman?
Coincidentally, Emily will be talking about the relation between Riehl-Verity and Riehl-Shulman about 2 hours from now in HoTTEST.
I had forgotten about that, your work with Emily is definitely very interesting. Is it in principle able to express the kind of translation principle we were discussing (from ordinary to -category theory, rather than between -categories)?
Incidentally, your work with Emily reminds me of something I am very interested in, which is a kind of syntactic version of (and development) Lawvere’s ideas of how to take the category (or, as I think we would certainly proceed nowadays, 2-category) of categories as a foundation. I definitely think introducing primitive types for things like a directed interval is the right approach.
Well, since not everything in 1-category theory translates to -category theory, there can’t be any direct “translation”. I think the best thing to hope for is some formal context that can be interpreted both into 1-category theory and -category theory. Then in place of a “translation” we have a “span” or “partial translation” whereby starting with some result in 1-category theory we have to ask “does it lift to the formal context?” or “can it be expressed in the formal language?”, and then if the answer is yes, we can then interpret that lifting into -category theory.
With this interpretation of the question, the answer for my work with Emily is “up to a point”. Our syntax is explicitly and heavily motivated by the Rezk model for -categories in the category of bisimplicial sets. We define syntactically objects called “Segal types” and “Rezk types” that correspond to Segal spaces and Rezk spaces (complete Segal spaces). Morally we should be working with the Rezk types as models of -categories, but in fact it turns out that many theorems are already valid for Segal types. Now I believe that our syntax also has an interpretation into simplicial sets, under which the Segal types correspond to (the nerves of) ordinary categories and the Rezk types correspond to categories in which every isomorphism is an identity. So any theorem of 1-category theory that can be lifted to a theorem about Segal types in our syntax is also true about -categories. But there are also true things our syntax can say about -categories (i.e. Rezk spaces) that don’t “lift backwards” to theorems about 1-categories since not every category is a Rezk type.
Our syntax is currently also a bit limited in the aspects of category theory it can talk about. For instance, we don’t have yet something corresponding to the category of sets/spaces, nor do we have any notion of “opposite category”. But it seems reasonable to hope that future developments may address these limitations.
I have also noticed the connection to CCAF. In fact, I noticed recently that Lawvere’s fundamental axiom is closely connected to the definition of Segal type: the Segal types are exactly the types that “internally think that ”.
Thanks! I find this interesting, and have begun looking at your paper in more detail.
One thing that precludes a semantics in Cat or Poset is the obvious point that you use an intensional dependent type theory as one of the layers (the cube and tope layers are no problem). Somehow this doesn’t seem really fundamental to me. Have you thought about whether a semantics in Cat might be possible if you somehow replace the intensional dependent type theory layer with something else?
Another point I am very interested in, which I believe is related to your last remark, is that the interval in your syntax has what I call ’strictness of identities’ as well as connections with good properties, which means morally (i.e. up to finding some kind of syntactical category in which to express the same kind of ideas) that one will be able to put a model structure on it by the methods of my thesis. Such a thing would be some kind of ’folk model structure’ for -categories.
Regarding defining something corresponding to sets/spaces, I have thought a bit about that in the past, and one idea I am quite keen on is to define Set to be the free co-completion of 1. Now, this may seem circular. But it does not seem to me impossible that one might be able to define a free co-completion 2-monad without actually referring to Set, if one’s ambient (i.e. axiomatic) 2-category of categories is sufficiently nice.
I played around a little with leaving out the identity types entirely and essentially taking Rezk-ness as the definition of identity types. But I wasn’t able to make it work short of putting in explicitly all the higher groupoid structure on such things in a cubical-type-theory-like way. My current feeling is that what makes the Riehl-Shulman theory pretty is that it can “piggyback” the homotopy-coherence of -categories on the homotopy-coherence of -groupoids that is ensured by the ambient HoTT, allowing us to express infinite coherence conditions like Segal-ness in a finitary way. But I highly encourage other people like you to think about this; there’s a lot of open ground for variations and improvements. Defining to be the free cocompletion of 1 might just be possible too, I look forward to hearing whether you can make it work.
Thanks for the thoughts! I’ve now begun a discussion of how to carry out free co-completion without referring to here.
1 to 13 of 13