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.
Thanks to Urs and the rest of the steering committee I now have a personal web. Feel free to use this thread to comment on anything you find there, or drop a comment box over there in the usual way.
Edit: never mind.
I finally submitted my thesis a couple of months ago, so I’ve put a brief not-yet-entirely-complete outline at thesis outline (finnlawler), for anyone who’s interested.
Congratulations! Kudos for delving into the world of tricategories, always seemed daunting to me.
Thanks, David! I should add that comments and questions are more than welcome.
I’ve rounded off my thesis outline (finnlawler), if anyone else would like to have a look. In particular, I’d be interested to hear if anyone has seen the first result under Tabulation and comprehension before, in this generality; I mean the equivalence for a predicate P over X in the bifibration E, where is the extension of P.
For what it’s worth, I haven’t seen this result, but then of course this doesn’t mean anything. But it seems to me a good insight for appreciating Lawvere’s axiomatization of comprehension. Since this equivalence has such a natural “meaning”, it makes one think if not full comprehension should be the default notion, and the other be re-named “pre-comprehension” or something.
But these days I am thinking everything in terms of dependent linear type theory, and that made me wonder if there is something to be found here. In the linear context one would want to take the -functor to be given by push-forward of the tensor unit. In the standard geometric models this is the push-forward of the structure sheaf as a (quasi-coherent) sheaf of modules. Then asking for that right adjoint to exist is some condition on this “image” being suitably invertible still, as a module, hence is something like the condition for a Wirthmüller isomorphism. And then “full comprehension” would translate to a statement relating morphisms of sheaves of modules to extensions of sheaves of modules.
Not sure if that leads anywhere, but this is what it made me think of. (And now hopefully somebody else here make a comment more to the actual point of your thesis…)
Finn: Congratulations from Anglesey! When will you have the oral?
Urs: the Wirthmüller stuff is interesting, although I can’t pretend to understand the context. But I would like to find out how much of this stuff works for monoidal fibrations that aren’t cartesian.
Tim: thanks! The viva hasn’t been scheduled yet; still waiting to hear back from the external examiners. I’m dreading it and looking forward to it in equal measure!
This is awesome; congrats! I’m looking forward to reading the whole thing. This definitely seems to me like the “right” point of view on cartesian bicategories. A couple of thoughts that occur to me from reading the outline:
As you may know, there are two notions of “monad 2-cell”: one which occurs in the 2-category and one which occurs in the free cocompletion under Kleisli objects, . These 2-categories have the same objects and morphisms, but the second kind of 2-cell is more general; references for the latter include “The formal theory of monads II” and 1301.3191. Are both of these “insufficiently lax” for your equipment 2-cells?
Presumably the correspondence between regular fibrations and regular equipments is closely related to the correspondence I showed here between sites and framed allegories?
As for your question, that result doesn’t ring a bell for me in that generality. It’s a nice one!
Thanks, Mike! Those are good questions:
Yes, neither gives what we want, which is colax transformations with tight components. A monad 2-cell gives a pseudonatural transformation whose components must be tight; a Kleisli 2-cell relaxes the latter condition, but doesn’t allow the transformation to be colax. I have an idea for how to get around this, but it will take more working out. (Loosely: a monad morphism in this context is a pseudo algebra for a certain pseudo monad, and the kind of 2-cell we want is a lax morphism between these algebras. Fitting all of these into a tricategory is the tricky part, but I’m hoping there will be enough lax morphism classifiers to simplify things.)
Yes, I would certainly expect so. I remember reading your paper with keen interest when it came out, and thinking it could be highly relevant to my work, but in the end I didn’t have the time to expand my stuff enough to connect it with yours. Of course, one issue is that what I’ve done only works in the presence of finite products, whereas I think I remember a conversation you, Todd and me had a while back where you said that you used allegories precisely because some of the sites you were dealing with didn’t have products. Again, I have an idea about how to generalize, but this one’s still rather vague.
1 to 11 of 11