Module model_morphism

Morphisms between models of double theories.

A morphism between models consists of functions between objects and between morphisms that are:

1. Well-typed: preserve object and morphism types
2. Functorial: preserve composition and identities
3. Natural: commute with object operations and morphism operations, possibly up to comparison maps

In mathematical terms, a model morphism is a natural transformation between lax double functors. The natural transformation can be strict, pseudo, lax, or oplax. For models of discrete double theories, all these options coincide.

References

• Paré 2011, Section 1.5: Natural transformations
• Lambert & Patterson 2024, Section 7: Lax transformations

Re-exports

pub use super::discrete::model_morphism::*;

Enums

InvalidDblModelMorphism

An invalid assignment in a morphism between models of a double theory.