Expand description
Virtual double categories.
§Background
A virtual double category (VDC) is like a double category, except that there is no external composition operation on proarrows or cells. Rather, a cell has a domain that is a path of proarrows (a “virtual” composite). The name “virtual double category” was introduced by Cruttwell and Shulman but the concept has gone by many other names, notably fc-multicategory (Leinster 2004).
Composites of proarrows in a VDC, if they exist, are represented by cells satsifying a universal property (Cruttwell-Shulman 2008, Section 5). In our usage of virtual double categories as double theories, we will assume that units (nullary composites) exist. We will not assume that any other composites exist, though often they do.
Virtual double categories have pros and cons compared with ordinary double
categories. We prefer VDCs in catlog because pastings of cells are much
simpler in a VDC than in a double category: a pasting diagram in VDC is a
well-typed tree of cells, rather than a kind of planar string
diagram, and the notorious
pinwheel obstruction
to composition in a double category does not arise in VDCs.
§Examples
A double theory is “just” a unital virtual double category, so any double theory in the standard library is an example of a VDC. For testing purposes, this module provides several minimal examples of VDCs implemented directly, namely “walking” categorical structures that can be interpreted in any VDC:
- the walking category
- the walking functor
- the walking bimodule or profunctor
The walking category and bimodule can be seen as discrete double theories, while the walking functor is a simple double theory, but here they are implemented at the type level rather than as instances of general data structures.
Modules§
- Walking
Bimodule - The walking bimodule as a VDC.
- Walking
Functor - The walking functor as a VDC.
Structs§
- FreeV
DblCategory - The VDC freely generated by a virtual double graph.
- Underlying
DblGraph - The underlying virtual double graph of a VDC.
- Walking
Category - The walking category as a VDC.
Traits§
- VDCWith
Composites - A virtual double category with some or all chosen composites.
- VDbl
Category - A virtual double category (VDC).