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.

References

• Lambert & Patterson 2024, Section 7: Lax transformations

Structs

• DblModelMorphism
  A functor between models of a double theory defined by a mapping.
• DiscreteDblModelMapping
  A mapping between models of a discrete double theory.
• DiscreteDblModelMorphismFinder
  Finds morphisms between two models of a discrete double theory.

Enums

• InvalidDblModelMorphism
  An invalid assignment in a double model morphism defined explicitly by data.

Traits

• DblModelMapping
  A mapping between models of a double theory.

Type Aliases

• DiscreteDblModelMorphism
  A morphism between models of a discrete double theory.