catlog/dbl/
computad.rs

1//! Computads for virtual double categories.
2
3use std::hash::Hash;
4
5use derivative::Derivative;
6use derive_more::Constructor;
7
8use super::graph::{InvalidVDblGraph, VDblGraph};
9use crate::one::{Graph, Path, ReflexiveGraph, ShortPath};
10use crate::zero::*;
11
12/// Top-dimensional data of an augmented virtual double computad.
13///
14/// Intended for use with [`AVDCComputad`].
15#[derive(Debug, Derivative)]
16#[derivative(Default(bound = ""))]
17pub struct AVDCComputadTop<Ob, Arr, Pro, Sq> {
18    squares: HashFinSet<Sq>,
19    dom: HashColumn<Sq, Path<Ob, Pro>>,
20    cod: HashColumn<Sq, ShortPath<Ob, Pro>>,
21    src: HashColumn<Sq, Arr>,
22    tgt: HashColumn<Sq, Arr>,
23}
24
25impl<Ob, Arr, Pro, Sq> AVDCComputadTop<Ob, Arr, Pro, Sq>
26where
27    Ob: Eq + Clone,
28    Arr: Eq + Clone,
29    Pro: Eq + Clone,
30    Sq: Eq + Clone + Hash,
31{
32    /// Adds a square to the double computad.
33    pub fn add_square(
34        &mut self,
35        sq: Sq,
36        dom: Path<Ob, Pro>,
37        cod: ShortPath<Ob, Pro>,
38        src: Arr,
39        tgt: Arr,
40    ) -> bool {
41        self.dom.set(sq.clone(), dom);
42        self.cod.set(sq.clone(), cod);
43        self.src.set(sq.clone(), src);
44        self.tgt.set(sq.clone(), tgt);
45        self.squares.insert(sq)
46    }
47}
48
49/// An augmented virtual double computad.
50///
51/// The set of objects and the graphs of arrows and proarrows are assumed already
52/// constructed, possibly from other generating data, while the top-dimensional
53/// generating data is provided directly.
54///
55/// We say "augmented" because the generating squares have co-arity zero or one,
56/// like the cells in an *augmented VDC* ([Koudenburg
57/// 2020](crate::refs::AugmentedVDCs)), though we use such computads to generate
58/// *unital* VDCs.
59#[derive(Constructor)]
60pub struct AVDCComputad<'a, Ob, Arr, Pro, ObSet, ArrGraph, ProGraph, Sq> {
61    objects: &'a ObSet,
62    arrows: &'a ArrGraph,
63    proarrows: &'a ProGraph,
64    computad: &'a AVDCComputadTop<Ob, Arr, Pro, Sq>,
65}
66
67impl<'a, Ob, Arr, Pro, ObSet, ArrGraph, ProGraph, Sq> VDblGraph
68    for AVDCComputad<'a, Ob, Arr, Pro, ObSet, ArrGraph, ProGraph, Sq>
69where
70    Ob: Eq + Clone,
71    Arr: Eq + Clone,
72    Pro: Eq + Clone,
73    Sq: Eq + Clone + Hash,
74    ObSet: Set<Elem = Ob>,
75    ArrGraph: Graph<V = Ob, E = Arr>,
76    ProGraph: ReflexiveGraph<V = Ob, E = Pro>,
77{
78    type V = Ob;
79    type E = Arr;
80    type ProE = Pro;
81    type Sq = Sq;
82
83    fn has_vertex(&self, v: &Self::V) -> bool {
84        self.objects.contains(v)
85    }
86    fn has_edge(&self, e: &Self::E) -> bool {
87        self.arrows.has_edge(e)
88    }
89    fn has_proedge(&self, p: &Self::ProE) -> bool {
90        self.proarrows.has_edge(p)
91    }
92    fn has_square(&self, sq: &Self::Sq) -> bool {
93        self.computad.squares.contains(sq)
94    }
95    fn dom(&self, e: &Self::E) -> Self::V {
96        self.arrows.src(e)
97    }
98    fn cod(&self, e: &Self::E) -> Self::V {
99        self.arrows.tgt(e)
100    }
101    fn src(&self, p: &Self::ProE) -> Self::V {
102        self.proarrows.src(p)
103    }
104    fn tgt(&self, p: &Self::ProE) -> Self::V {
105        self.proarrows.tgt(p)
106    }
107    fn square_dom(&self, sq: &Self::Sq) -> Path<Self::V, Self::ProE> {
108        self.computad.dom.apply_to_ref(sq).expect("Domain of square should be defined")
109    }
110    fn square_cod(&self, sq: &Self::Sq) -> Self::ProE {
111        self.computad
112            .cod
113            .apply_to_ref(sq)
114            .expect("Codomain of square should be defined")
115            .as_edge(self.proarrows)
116    }
117    fn square_src(&self, sq: &Self::Sq) -> Self::E {
118        self.computad.src.apply_to_ref(sq).expect("Source of square should be defined")
119    }
120    fn square_tgt(&self, sq: &Self::Sq) -> Self::E {
121        self.computad.tgt.apply_to_ref(sq).expect("Target of square should be defined")
122    }
123    fn arity(&self, sq: &Self::Sq) -> usize {
124        self.computad.dom.get(sq).expect("Domain of square should be defined").len()
125    }
126}
127
128impl<'a, Ob, Arr, Pro, ObSet, ArrGraph, ProGraph, Sq>
129    AVDCComputad<'a, Ob, Arr, Pro, ObSet, ArrGraph, ProGraph, Sq>
130where
131    Ob: Eq + Clone,
132    Arr: Eq + Clone,
133    Pro: Eq + Clone,
134    Sq: Eq + Clone + Hash,
135    ArrGraph: Graph<V = Ob, E = Arr>,
136    ProGraph: Graph<V = Ob, E = Pro>,
137{
138    /// Iterates over failures to be a valid virtual double graph.
139    ///
140    /// Note that this method *assumes* that the graphs of objects and (pro)arrows
141    /// are already valid. If that is in question, validate them first.
142    pub fn iter_invalid<E, ProE>(&self) -> impl Iterator<Item = InvalidVDblGraph<E, ProE, Sq>> {
143        let cptd = self.computad;
144        cptd.squares.iter().flat_map(|sq| {
145            let (dom, cod) = (cptd.dom.get(&sq), cptd.cod.get(&sq));
146            let (src, tgt) = (cptd.src.get(&sq), cptd.tgt.get(&sq));
147            let mut errs = Vec::new();
148            if !dom.is_some_and(|path| path.contained_in(self.proarrows)) {
149                errs.push(InvalidVDblGraph::SquareDom(sq.clone()));
150            }
151            if !cod.is_some_and(|path| path.contained_in(self.proarrows)) {
152                errs.push(InvalidVDblGraph::SquareCod(sq.clone()));
153            }
154            if !src.is_some_and(|f| self.arrows.has_edge(f)) {
155                errs.push(InvalidVDblGraph::SquareSrc(sq.clone()));
156            }
157            if !tgt.is_some_and(|g| self.arrows.has_edge(g)) {
158                errs.push(InvalidVDblGraph::SquareTgt(sq.clone()));
159            }
160            if errs.is_empty() {
161                let (m, n, f, g) = (dom.unwrap(), cod.unwrap(), src.unwrap(), tgt.unwrap());
162                if !(m.src(self.proarrows) == self.arrows.src(f)
163                    && m.tgt(self.proarrows) == self.arrows.src(g)
164                    && n.src(self.proarrows) == self.arrows.tgt(f)
165                    && n.tgt(self.proarrows) == self.arrows.tgt(g))
166                {
167                    errs.push(InvalidVDblGraph::NotSquare(sq));
168                }
169            }
170            errs.into_iter()
171        })
172    }
173}
catlog/dbl/computad.rs

catlog/dbl/
computad.rs
