Proposition [efr-002Y]

Let \mathcal {C} be a bicategory, and let \mathcal {C}_0 \to \mathcal {C} be an identity-on-objects functor from a 1-category. Then there is a pseudo double category where

1. The objects are the objects of \mathcal {C}
2. The vertical category is \mathcal {C}_0
3. The horizontal category is \mathcal {C}
4. A 2-cell is a 2-cell in \mathcal {C} filling the square