# 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.

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

- Every restriction category gives a double category.

# all_double_categories (view)

### 5 rows

This data as json, CSV (advanced)

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

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;