Module category

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 satisfying 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 they often do. Like anything defined by a universal property, composites are not strictly unique if they exist but they are unique up to unique isomorphism. As often when working with (co)limits, our trait for virtual double categories assumes that a choice of composites has been made whenever they are needed. We do not attempt to “recognize” whether an arbitrary cell has the relevant universal property.

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.

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

• WalkingBimodule
  The walking bimodule as a VDC.
• WalkingFunctor
  The walking functor as a VDC.

Structs

• FreeVDblCategory
  The VDC freely generated by a virtual double graph.
• UnderlyingDblGraph
  The underlying virtual double graph of a VDC.
• WalkingCategory
  The walking category as a VDC.

Traits

• VDblCategory
  A virtual double category (VDC).