Module model

Models of double theories.

A model of a double theory is a category (or categories) equipped with operations specified by the theory, categorifying the familiar idea from logic that a model of a theory is a set (or sets) equipped with operations. For background on double theories, see the theory module.

In the case of a simple double theory, which amounts to a small double category, a model of the theory is a span-valued lax double functor out of the theory. Such a model is a “lax copresheaf,” categorifying the notion of a copresheaf or set-valued functor. Though they are “just” lax double functors, models come with extra intuitions. To bring that out we introduce new jargon, building on that for double theories.

Terminology

A model of a double theory consists of elements of two kinds:

1. Objects, each assigned an object type in the theory;

2. Morphisms, each having a domain and a codomain object and assigned a morphism type in the theory, compatibly with the domain and codomain types;

In addition, a model has the following operations:

• Object action: object operations in the theory act on objects in the model to produce new objects;

• Morphism action: morphism operations in the theory act on morphisms in the model to produce new morphisms, compatibly with the object action;

• Composition: a path of morphisms in the model has a composite morphism, whose type is the composite of the corresponding morphism types.

Structs

• DiscreteDblModel
  A finitely presented model of a discrete double theory.
• DiscreteTabModel
  A finitely presented model of a discrete tabulator theory.

Enums

• InvalidDblModel
  A failure of a model of a double theory to be well defined.
• TabEdge
  “Edge” in a model of a discrete tabulator theory.
• TabOb
  Object in a model of a discrete tabulator theory.

Traits

• DblModel
  A model of a double theory.
• FgDblModel
  A finitely generated model of a double theory.
• MutDblModel
  A mutable, finitely generated model of a double theory.

Type Aliases

• TabMor
  Morphism in a model of a discrete tabulator theory.
• UstrDiscreteDblModel
  A model of a discrete double theory where both theoy and model have keys of type Ustr.
• UstrDiscreteTabModel
  A model of a discrete tabulator theory where both theory and model have keys of type Ustr.