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
    • Part I, 1999: Limits in double categories (pdf)
    • Part II, 2004: Adjoint for double categories (pdf)
    • Part III, 2008: Kan extensions in double categories (pdf)
    • Part IV, 2007: Lax Kan extensions for double categories (pdf)
  • Paré, 2011: Yoneda theory for double categories (pdf, slides)
    • Paré, 2013: Composition of modules for lax functors (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:

  • Paré, 2021: Morphisms of rings (doi, pdf)

Applications to logic and PLT:

  • Bruni, Meseguer, Montanari, 2002: Symmetric monoidal and cartesian double categories as a semantic framework for tile logic (doi)
    • Based on 1998 tech report: Process and term title logic (pdf)
    • Bruni & Montanari, 1999: Cartesian closed double categories, their lambda-notation, and the pi-calculus (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