Lately I’ve been pursuing formal category theory using double categories. A first step in this program is to abstract from categories to category objects in a double category; for instance, internal categories are category objects in a double category of spans and enriched categories are category objects in a double category of matrices. The next step is to take structures defined on categories and generalize them to category objects in a double category. By the microcosm principle, that is possible when the double category possesses a categorified version of the very structure in question. The concepts from double category theory that I’ve used so far, like products and coproducts, indeed categorify familiar concepts from category theory. While there are interesting twists along the way,1 the one-dimensional story gives strong hints about how to generalize to double categories.
This is a companion discussion topic for the original entry at https://topos.institute/blog/2024-06-20-compact-double-categories-1/