Double categories
A double category is a category (or pseudocategory) internal to Cat. Double categories were invented by Ehresmann in the early 60s, making them the first higher-dimensional categorical structure. Double categories have long been eclipsed by bicategories but they now seem to making a comeback. Unfortunately, the theory of double categories is still much less developed than that of 2-categories and bicategories.
Examples
- A 2-category is a double category whose proarrows are all identities, whereas a bicategory is a (pseudo) double category whose arrows are all identities
- The arrow category of a category is a double category
- More generally, any 2-category has a double category of quintets
- The double category of sets, functions, and spans (alternatively, relations)
- Categorifying, the double category of categories, functors, and profunctors
- The double category of rings, ring homomorphisms, and bimodules (Paré, 2021)
Further examples are in (Grandis & Paré, 1999, Sec. 3: “Examples of double and pseudo double categories”).
Literature
Books and surveys
- Kelly & Street, 1974: Review of the elements of 2-categories
- Sec. 1: Defines strict double categories and, as special case, 2-categories
- But main focus is on 2-categories
- Myers, 2017: String diagrams for double categories and equipments (arxiv, nCat Cafe )
- Grandis, 2019: Higher dimensional categories: From double to multiple
categories (doi), Part I: From categories to double categories
- The most complete general reference for double categories available today
- Niefield, 2021, lectures: Introduction to double categories (video 1 ,2 , slides 1 ,2 )
General theory
- Dawson & Paré, 1993: General associativity and general composition for double
categories (pdf)
- Proves two-dimensional associativity of composition of cells
- Grandis & Paré, series: On weak double categories
- Paré, 2011: Yoneda theory for double categories (pdf, slides)
- Niefield, 2012: Span, cospan, and other double categories (pdf, arxiv)
- Grandis & Paré, 2017: Span and cospan representations of weak double categories (pdf)
- Lambert, 2021: Discrete double fibrations (pdf, arxiv)
- Crutwell, Lambert, et al, 2022: Double fibrations (arxiv)
Free constructions on double categories
As with other categorical structures, free constructions involving double categories and double functors lead to rich combinatorcs.
- Dawson & Paré, 2002: What is a free double category like? (doi)
- Dawson, Paré, Pronk, 2003: Adjoining adjoints (doi)
- Constructs the 2-category that freely adjoins right adjoints to a category, viewed as a locally discrete 2-category
- Dawson, Paré, Pronk, 2003: Undecidability of the free adjoint construction (doi)
- Dawson, Paré, Pronk, 2004: Free extensions of double categories (pdf)
- Dawson, Paré, Pronk, 2006: Paths in double categories (pdf)
- Dawson, Paré, Pronk, 2004: Universal properties of Span (pdf)
- Dawson, Paré, Pronk, 2006: The span construction (pdf)
- Delpeuch, 2020: The word problem for double categories (arxiv, pdf)
- Reduces the word problem for free double categories to the word problem for 2-categories
Equipments and monoidal double categories
- Dawson, Paré, Pronk, 2006: The span construction (pdf)
- Discusses double categories with companions and conjoints under the name “gregarious double categories” (!)
- Shulman, 2008: Framed bicategories and monoidal fibrations (pdf, arxiv)
- Introduces framed bicategories (which are really double categories), equivalent to proarrow equipments (which actually are bicategories)
- Sec. 2: Clearly defines (pseudo) double categories with many examples
- Shulman, 2010: Constructing symmetric monoidal bicategories (arxiv, nCat Cafe )
- Here framed bicategories are renamed to fibrant double categories
- Explains how to convert monoidal double categories to monoidal bicategories
- Sec. 2: Clearly defines (pseudo) double categories and symmetric monoidal double categories
- Remark 2.11 is about cartesian bicategories
- Hansen & Shulman, 2019: Constructing symmetric monoidal bicategories functorially (arxiv)
- Aleiferi, 2018, PhD thesis: Cartesian double categories with an emphasis on characterizing spans (arxiv, nCat Cafe )
- Lambert, 2021: Double categories of relations (arxiv)
Examples and applications
Applications to algebra:
Applications to logic and PLT:
- Bruni, Meseguer, Montanari, 2002: Symmetric monoidal and cartesian double categories as a semantic framework for tile logic (doi)
- Mellies, 2002: Double categories: a modular model of multiplicative linear
logic (doi)
- Sec. 1 motivates double categories as device for modular rewriting of lambda terms, a refinement of rewriting via 2-categories
- Sec. 1 includes nice overview of history of linear logic in categorical proof theory