I want to define a notion of cartesian equipment, the idea being that a bicategory should be a cartesian bicategory if and only if the proarrow equipment is a cartesian equipment.
This shouldn’t be hard to do. There are three notions of equipment in the literature:
Wood’s: an identity-on-objects, locally fully faithful pseudofunctor , written , where each has a right adjoint in .
Shulman’s: a framed bicategory, that is, a pseudo double category whose source and target functors form a bifibration.
that of Carboni–Kelly–Verity–Wood: a (normal) pseudofunctor , where is a 1-category.
The last is strictly more general than the others, as are even their starred pointed equipments, i.e. those equipped with a transformation , where the left and right actions of have suitable adjoints. These CKVW equipments should be equivalent to the others if we ask for a transformation making a (pseudo)monad in a suitable bi- or tricategory of ‘biprofunctors’.
Question: Why are these all equivalent?
An identity-on-objects (pseudo)functor that is locally fully faithful is essentially the same thing as an identity-on-objects functor out of a locally discrete bicategory. In the case of strict 2-categories, these are (by some enriched-category nonsense) precisely the Kleisli objects for monads (on locally discrete strict 2-categories) in . The Grothendieck construction for such a profunctor should give a double category whose underlying span is a two-sided fibration.
With the correct notion of equipment, there are two possible notions of adjoint morphisms, and hence limits: those of CKVW, and those of Grandis–Paré (for double categories).
Question: Do these notions coincide?
Then a cartesian equipment will be an equipment that ‘has finite products’, that is an equipment for which the diagonals and have right pseudoadjoints.