Add support for double categories

[varkor]

As written in this comment:

If someone opens a separate issue listing, say, 10 concrete and interesting examples of double categories together with 20 concrete properties, I will definitely add support for them.

The following are given without explanation for now, but I can add context on request. I merely wanted to illustrate that there certainly are enough concrete examples and properties of interest.

Examples of double categories

• Sq(Set)
• Span
• Rel
• SMult
• Par
• Dist
• RingMod
• Poly
• Comod(Poly)
• The double category whose objects are toposes, tight morphisms are geometric morphisms (in the algebraic direction), and loose morphisms are lex functors.

Properties of double categories

• Has companions
• Has conjoints
• Is replete (has companions/conjoints of invertible tight morphisms specifically)
• Has tabulators
• Has effective tabulators
• Has limits of loose comonads
• Has local limits
• Has parallel limits
• Is cartesian closed
• Has power objects
• Has (right) lifts
• Has (right) extensions
• Is exact
• Is Cauchy
• Is right-connected
• Is locally preordered
• Is strict
• Is crossed
• Is unit-pure
• Is a double category of relations

[dschepler]

Are these what nLab calls M-categories, i.e. categories enriched over the category Mono consisting of a set and a distinguished subset, with the cartesian monoidal structure?

[ScriptRaccoon]

@dschepler Double categories are categories internal to Cat, https://ncatlab.org/nlab/show/double+category. M-categories are different.

[varkor]

Every M-category (and, more generally, every F-category) induces a double category, but not every double category is of this form.

On a separate note, for double categories it will be necessary to have two kinds of duality (in the tight and in the loose directions) for each property and example.

[ScriptRaccoon]

@varkor Since you speak of loose and tight morphisms: Do you refer to "pseudo double categories" in this issue?

[varkor]

Yes, though this would include strict double categories as a special case.