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.