Embedding conjecture for weak double categories and double bicategories

A weak double category is a pseudo-category object in pseudo-categories with a set of squares, while a double bicategory is Verity's corresponding weak structure. A double bicategory is doubly weak when its horizontal and vertical bicategories coincide with the bicategories formed from its objects, horizontal and vertical morphisms, and squares whose opposite edges are identities.

Embedding conjecture. There is a fully faithful embedding of weak double categories into Verity's double bicategories with essential image given by double bicategories in which the given horizontal (vertical) bicategory coincides with the bicategory given by objects, horizontal (vertical) morphisms and squares whose vertical (horizontal) edges are identities.

The condition on the essential image is a bicategorical completeness condition ensuring well-defined underlying horizontal and vertical bicategories. If true, it would place strict double categories, weak double categories, and double bicategories in a chain of inclusions.