pub trait DblModel: Category {
type ObType: Eq;
type MorType: Eq;
type ObOp: Eq;
type MorOp: Eq;
type Theory: DblTheory<ObType = Self::ObType, MorType = Self::MorType, ObOp = Self::ObOp, MorOp = Self::MorOp>;
// Required methods
fn theory(&self) -> &Self::Theory;
fn ob_type(&self, x: &Self::Ob) -> Self::ObType;
fn mor_type(&self, m: &Self::Mor) -> Self::MorType;
fn ob_act(&self, x: Self::Ob, f: &Self::ObOp) -> Self::Ob;
fn mor_act(&self, m: Self::Mor, α: &Self::MorOp) -> Self::Mor;
}Expand description
A model of a double theory.
As always in logic, a model makes sense only relative to a theory, but a theory can have many different models. So, in Rust, a model needs access to its theory but should not own its theory. Implementors of this trait might use an immutable shared reference to the theory.
Objects and morphisms in a model are typed by object types and morphism types in
the theory. There is a design choice about whether identifiers for objects
(Ob) and morphisms (Mor) are unique
relative to their types or globally within the model. If we took the first
approach (as we do in the Julia package
ACSets.jl), one could only make
sense of objects and morphisms when their types are known, so the early methods
in the trait would look like this:
fn has_ob(&self, x: &Self::Ob, t: &Self::ObType) -> bool;
fn has_mor(&self, m: &Self::Mor, t: &Self::MorType) -> bool;
fn dom(&self, m: &Self::Mor, t: &Self::MorType) -> Self::Ob;
fn cod(&self, m: &Self::Mor, t: &Self::MorType) -> Self::Ob;It will be more convenient for us to take the second approach since in our usage object and morphism identifiers will be globally unique in a very strong sense (something like UUIDs).