You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
From every double category , we can extract its vertical category and its horizontal bicategory.
If is the double category of categories, functors and profunctors, then we recover as vertical category the category of categories and functors and as horizontal bicategory the bicategory of categories, profunctors and natural transformations between them.
But possesses more structure: its vertical category is not only a category but also a 2-category.
And it doesn't seem to be a consequence of the definition of a double category than the vertical category is a 2-category. It doesn't seem either to be a consequence of the definition of proarrow equipment.
Do you know other double categories such that the vertical category is a 2-category? Should we then impose additional coherences on this object: "a double category whose vertical category is a 2-category" and give a definition which encompass such situations?
It is a consequence of the definition of a double category. Just take the definition of the horizontal bicategory and transpose it. You have to compose with the unit isomorphisms for horizontal composition when composing 2-cells, but it all works out.
Oh thank you!
But I'm not sure that it is exactly what I want. The 2-cells in the double category of profunctors that you compose to get a 2-category as you say are not the natural transformations between functors, they are the natural transformations between parallel profunctors. What I would want is to get as 2-cells the natural transformations between functors and this not what we obtain here.
From a bicategory, I obtain a 2-category with 0-cells the objects, 1-cells the proarrows and 2-cells the 2-cells of the double category with left and right frames the identity, is it what you say?
No, that's the horizontal bicategory. I mean the 0-cells are the objects (e.g. categories), the 1-cells are the arrows (e.g. functors), and the 2-cells are the squares of the double category with top and bottom frames the identity. You can check that a square of that sort in Cat is equivalent to an ordinary natural transformation between its left and right framing functors.
Ok, thanks, it works perfectly.