Monoidal double category of categories

See also

• formal category theory