Module model_diagram

Diagrams in models of a double theory.

A diagram in a model is simply a morphism into that model. This includes the domain of that morphism, which is assumed to be a free model.

Diagrams are currently used primarily to represent instances of models from a fibered perspective, generalizing how a diagram in a category can be used to represent a copresheaf over that category.

References

TODO: Document in devs docs and link here.

Structs

• DblModelDiagram
  A diagram in a model of a double theory.

Enums

• InvalidDblModelDiagram
  A failure of a diagram in a model to be valid.

Type Aliases

• DiscreteDblModelDiagram
  A diagram in a model of a discrete double theory.
• InvalidDiscreteDblModelDiagram
  A failure to be valid in a diagram in a model of a discrete double theory.