Trait VDCWithComposites

Source

pub trait VDCWithComposites: VDblCategory {
    // Required methods
    fn composite_ext(
        &self,
        path: Path<Self::Ob, Self::Pro>,
    ) -> Option<Self::Cell>;
    fn through_composite(
        &self,
        cell: Self::Cell,
        range: Range<usize>,
    ) -> Option<Self::Cell>;

    // Provided methods
    fn has_composite(&self, path: &Path<Self::Ob, Self::Pro>) -> bool { ... }
    fn has_unit(&self, x: &Self::Ob) -> bool { ... }
    fn composite2_ext(&self, m: Self::Pro, n: Self::Pro) -> Option<Self::Cell> { ... }
    fn composite(&self, path: Path<Self::Ob, Self::Pro>) -> Option<Self::Pro> { ... }
    fn composite2(&self, m: Self::Pro, n: Self::Pro) -> Option<Self::Pro> { ... }
    fn unit_ext(&self, x: Self::Ob) -> Option<Self::Cell> { ... }
    fn unit(&self, x: Self::Ob) -> Option<Self::Pro> { ... }
    fn through_unit(&self, cell: Self::Cell, index: usize) -> Option<Self::Cell> { ... }
}

Expand description

A virtual double category with some or all chosen composites.

Like anything defined by a universal property, composites in a VDC are not strictly unique if they exist but they are unique up to unique isomorphism. As often when working with (co)limits, this trait assumes that a choice of composites has been made whenever they are exist. We do not attempt to “recognize” whether an arbitrary cell has the relevant universal property.

Required Methods§

Source

fn composite_ext(&self, path: Path<Self::Ob, Self::Pro>) -> Option<Self::Cell>

Gets the chosen cell witnessing a composite of proarrows, if there is one.

Such a cell is called an **extension or opcartesian cell.

Source

fn through_composite( &self, cell: Self::Cell, range: Range<usize>, ) -> Option<Self::Cell>

Factorizes a cell through a composite of proarrows.

The subpath of the domain path at the given range is replaced with the composite of that subpath, if the composite exists. This is the universal property of the composite.