Module theory

Double theories.

A double theory specifies a categorical structure, meaning a category (or categories) equipped with extra structure. The spirit of the formalism is that a double theory is “just” a virtual double category, categorifying Lawvere’s idea that a theory is “just” a category. Thus, a double theory is a concept with an attitude. To bring out these intuitions, the interface for double theories, DblTheory, introduces new terminology compared to the references cited below.

Terminology

A double theory comprises four kinds of things:

1. Object type, interpreted in models as a set of objects.

2. Morphism type, having a source and a target object type and interpreted in models as a span of morphisms (or heteromorphisms) between sets of objects.

3. Object operation, interpreted in models as a function between sets of objects.

4. Morphism operation, having a source and target object operation and interpreted in models as map between spans of morphisms.

The dictionary between the type-theoretic and double-categorical terminology is summarized by the table:

Associated type	Double theory	Double category	Interpreted as
ObType	Object type	Object	Set
MorType	Morphism type	Proarrow (loose morphism)	Span
ObOp	Object operation	Arrow (tight morphism)	Function
MorOp	Morphism operation	Cell	Map of spans

Models of a double theory are categorical structures, rather than merely set-theoretical ones, because each object type is assigned not just a set of objects but also a span of morphisms between those objects, constituting a category. The morphisms come from a distinguished “Hom” morphism type for each object type in the double theory. Similarly, each object operation is not just a function but a functor because it comes with an “Hom” operation between the Hom types. Moreover, morphism types can be composed to give new ones, as summarized by the table:

Method	Double theory	Double category
hom_type	Hom type	Identity proarrow
hom_op	Hom operation	Identity cell on arrow
compose_types	Compose morphism types	Compose proarrows

Finally, operations on both objects and morphisms have identities and can be composed:

Method	Double theory	Double category
id_ob_op	Identity operation on object type	Identity arrow
id_mor_op	Identity operation on morphism type	Identity cell on proarrow
compose_ob_ops	Compose object operations	Compose arrows
compose_mor_ops	Compose morphism operations	Compose cells

References

• Lambert & Patterson, 2024
• Patterson, 2024, Section 10: Finite-product double theories

Structs

• DiscreteDblTheory
  A discrete double theory.
• DiscreteTabTheory
  A discrete tabulator theory.
• TabMorOp
  Operation on morphisms in a discrete tabulator theory.

Enums

• TabMorProj
  Projection onto morphism type in a discrete tabulator theory.
• TabMorType
  Morphism type in a discrete tabulator theory.
• TabObProj
  Projection onto object type in a discrete tabulator theory.
• TabObType
  Object type in a discrete tabulator theory.

Traits

• DblTheory
  A double theory.

Type Aliases

• TabObOp
  Operation on objects in a discrete tabulator theory.
• UstrDiscreteDblTheory
  A discrete double theory with keys of type Ustr.
• UstrDiscreteTabTheory
  Discrete tabulator theory with names of type Ustr.