Expand description
Morphisms between models of double theories.
A morphism between models consists of functions between objects and between morphisms that are:
- Well-typed: preserve object and morphism types
- Functorial: preserve composition and identities
- 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.
§References
- Lambert & Patterson 2024, Section 7: Lax transformations
Structs§
- DblModel
Morphism - A functor between models of a double theory defined by a mapping.
- Discrete
DblModel Mapping - A mapping between models of a discrete double theory.
- Discrete
DblModel Morphism Finder - Finds morphisms between two models of a discrete double theory.
Enums§
- Invalid
DblModel Morphism - An invalid assignment in a double model morphism defined explicitly by data.
Traits§
- DblModel
Mapping - A mapping between models of a double theory.
Type Aliases§
- Discrete
DblModel Morphism - A morphism between models of a discrete double theory.