Double Categories

A double category is a generalized 2-category. A 2-category has objects, arrows, and natural transformations; arrows have one type of composition, but natural transformations have two types of composition, vertical and horizontal composition. A double category has two types of arrows, vertical and horizontal arrows, as well as natural transformations.

Every 2-category can be regarded as a double category with only one type of arrow. Similarly, every category can be regarded as a double category with only one type of arrow, using commuting squares of arrows for natural transformations. Every category's slice and coslice categories can be paired to form a double category.

By the Macrocosm Principle, there is a category DblCat whose objects are double categories and arrows are double functors; this is the category of internal categories in Cat. There are two functors which designate the 2-categories resulting from restricting the vertical and horizontal arrows respectively to identities; they are known as the horizontal and vertical 2-categories.

𝓗, 𝓥 : DblCat → 2Cat

There are several common constructions for double categories which are included from other tables:

5 rows sorted by kind

View and edit SQL

Suggested facets: 2cells_hr, kind

vertical_2cat horizontal_2cat 2cells_hr kind ▼
Lex Topos natural transformations plain
Prof Cat natural transformations plain
Rel Set subrelation inclusions plain
Set Pfn equivalences of restricted arrows total restriction
Top AdmRep equivalences of restricted arrows total restriction

Advanced export

JSON shape: default, array, newline-delimited

CSV options:

CREATE VIEW "all_double_categories" AS select vertical_2cat, horizontal_2cat, `2cells_hr`, 'plain' as kind from double_categories
UNION
select total_subcategory, partial_category, 'equivalences of restricted arrows', 'total restriction' from restriction_categories;