Trait DblTheory

pub trait DblTheory {
    type ObType: Eq + Clone;
    type MorType: Eq + Clone;
    type ObOp: Eq + Clone;
    type MorOp: Eq + Clone;

    // Required methods
    fn has_ob_type(&self, x: &Self::ObType) -> bool;
    fn has_mor_type(&self, m: &Self::MorType) -> bool;
    fn has_ob_op(&self, f: &Self::ObOp) -> bool;
    fn has_mor_op(&self, α: &Self::MorOp) -> bool;
    fn src_type(&self, m: &Self::MorType) -> Self::ObType;
    fn tgt_type(&self, m: &Self::MorType) -> Self::ObType;
    fn ob_op_dom(&self, f: &Self::ObOp) -> Self::ObType;
    fn ob_op_cod(&self, f: &Self::ObOp) -> Self::ObType;
    fn src_op(&self, α: &Self::MorOp) -> Self::ObOp;
    fn tgt_op(&self, α: &Self::MorOp) -> Self::ObOp;
    fn mor_op_dom(&self, α: &Self::MorOp) -> Path<Self::ObType, Self::MorType>;
    fn mor_op_cod(&self, α: &Self::MorOp) -> Self::MorType;
    fn compose_types(
        &self,
        path: Path<Self::ObType, Self::MorType>,
    ) -> Option<Self::MorType>;
    fn compose_ob_ops(&self, path: Path<Self::ObType, Self::ObOp>) -> Self::ObOp;
    fn compose_mor_ops(
        &self,
        tree: DblTree<Self::ObOp, Self::MorType, Self::MorOp>,
    ) -> Self::MorOp;

    // Provided methods
    fn hom_type(&self, x: Self::ObType) -> Self::MorType { ... }
    fn id_ob_op(&self, x: Self::ObType) -> Self::ObOp { ... }
    fn id_mor_op(&self, m: Self::MorType) -> Self::MorOp { ... }
}

A double theory.

A double theory is “just” a virtual double category (VDC) assumed to have units. Reflecting this, this trait has a blanket implementation for any VDblCategory. It is not recommended to implement this trait directly.

See the module-level docs for background on the terminology.

Required Associated Types

type ObType: Eq + Clone

Rust type of object types in the theory.

Viewing the double theory as a virtual double category, this is the type of objects.

type MorType: Eq + Clone

Rust type of morphism types in the theory.

Viewing the double theory as a virtual double category, this is the type of proarrows.

type ObOp: Eq + Clone

Rust type of operations on objects in the double theory.

Viewing the double theory as a virtual double category, this is the type of arrows.

type MorOp: Eq + Clone

Rust type of operations on morphisms in the double theory.

Viewing the double theory as a virtual double category, this is the type of cells.

Required Methods

fn has_ob_type(&self, x: &Self::ObType) -> bool

Does the object type belong to the theory?

fn has_mor_type(&self, m: &Self::MorType) -> bool

Does the morphism type belong to the theory?

fn has_ob_op(&self, f: &Self::ObOp) -> bool

Does the object operation belong to the theory?

fn has_mor_op(&self, α: &Self::MorOp) -> bool

Does the morphism operation belong to the theory?

fn src_type(&self, m: &Self::MorType) -> Self::ObType

Source of a morphism type.

fn tgt_type(&self, m: &Self::MorType) -> Self::ObType

Target of a morphism type.

fn ob_op_dom(&self, f: &Self::ObOp) -> Self::ObType

Domain of an operation on objects.

fn ob_op_cod(&self, f: &Self::ObOp) -> Self::ObType

Codomain of an operation on objects.

fn src_op(&self, α: &Self::MorOp) -> Self::ObOp

Source operation of an operation on morphisms.

fn tgt_op(&self, α: &Self::MorOp) -> Self::ObOp

Target operation of an operation on morphisms.

fn mor_op_dom(&self, α: &Self::MorOp) -> Path<Self::ObType, Self::MorType>

Domain of an operation on morphisms, a path of morphism types.

fn mor_op_cod(&self, α: &Self::MorOp) -> Self::MorType

Codomain of an operation on morphisms, a single morphism type.

fn compose_types( &self, path: Path<Self::ObType, Self::MorType>, ) -> Option<Self::MorType>

Composes a sequence of morphism types, if they have a composite.

fn compose_ob_ops(&self, path: Path<Self::ObType, Self::ObOp>) -> Self::ObOp

Compose a sequence of operations on objects.

fn compose_mor_ops( &self, tree: DblTree<Self::ObOp, Self::MorType, Self::MorOp>, ) -> Self::MorOp

Compose operations on morphisms.

Provided Methods

fn hom_type(&self, x: Self::ObType) -> Self::MorType

Hom morphism type on an object type.

Viewing the double theory as a virtual double category, this is the unit proarrow on an object.

fn id_ob_op(&self, x: Self::ObType) -> Self::ObOp

Identity operation on an object type.

View the double theory as a virtual double category, this is the identity arrow on an object.

fn id_mor_op(&self, m: Self::MorType) -> Self::MorOp

Identity operation on a morphism type.

Viewing the double theory as a virtual double category, this is the identity cell on a proarrow.

Implementors

impl<VDC: VDblCategory> DblTheory for VDC

type ObType = <VDC as VDblCategory>::Ob

type MorType = <VDC as VDblCategory>::Pro

type ObOp = <VDC as VDblCategory>::Arr

type MorOp = <VDC as VDblCategory>::Cell