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.
I started comma double category. Since I care about equipments more than double categories in general, and because it actually is an instance of a comma object, I made the article mostly about virtual double categories. I wrote down a couple of conjectures about when the comma has units and composites, but haven’t verified them yet and not sure when I will.
A good start, thanks! I agree that your conjectures are true, because (e.g. in the second case) the F-category of pseudo double categories and strong and lax double functors has comma objects of strong functors over lax ones, since they are a rigged limit.
One of my long-term projects is to find an abstract context in which to talk about things like comma objects of oplax over lax functors. I feel like it should have something to do with the fact that there’s a double category whose horizontal and vertical arrows are oplax and lax functors respectively, since the squares in the latter are exactly the right shape to be the universal 2-cell of such a comma object, but I haven’t found a good way to formulate the universal property yet.
I added some information about the colax/lax case, and the example of Dialectica constructions.
Mike, in your description of the Dialectica construction is an internal poset just a monad in span that is jointly monic?
Yes, since a monad in Span is an internal category. (Well, to be more precise an internal category with joinly-monic is an internal preorder, but who’s counting.)
1 to 6 of 6