catlog/dbl/discrete_tabulator/
theory.rs

1//! Discrete tabulator theories.
2
3use std::hash::Hash;
4use std::ops::Range;
5
6use derive_more::From;
7use ref_cast::RefCast;
8
9use crate::dbl::{category::*, graph::ProedgeGraph, tree::DblTree};
10use crate::one::{Graph, Path};
11use crate::zero::pretty::*;
12use crate::zero::*;
13
14/// Object type in a discrete tabulator theory.
15#[derive(Clone, Debug, PartialEq, Eq, Hash, From)]
16pub enum TabObType {
17    /// Basic or generating object type.
18    #[from]
19    Basic(QualifiedName),
20
21    /// Tabulator of a morphism type.
22    Tabulator(Box<TabMorType>),
23}
24
25/// Morphism type in a discrete tabulator theory.
26#[derive(Clone, Debug, PartialEq, Eq, Hash, From)]
27pub enum TabMorType {
28    /// Basic or generating morphism type.
29    #[from]
30    Basic(QualifiedName),
31
32    /// Hom type on an object type.
33    Hom(Box<TabObType>),
34}
35
36impl ToDoc for TabObType {
37    fn to_doc<'a>(&self) -> D<'a> {
38        match self {
39            TabObType::Basic(name) => name.to_doc(),
40            TabObType::Tabulator(mor_type) => unop(t("Tab"), mor_type.to_doc()),
41        }
42    }
43}
44
45impl ToDoc for TabMorType {
46    fn to_doc<'a>(&self) -> D<'a> {
47        match self {
48            TabMorType::Basic(name) => name.to_doc(),
49            TabMorType::Hom(ob_type) => unop(t("Hom"), ob_type.to_doc()),
50        }
51    }
52}
53
54/// Projection onto object type in a discrete tabulator theory.
55#[derive(Clone, Debug, PartialEq, Eq)]
56pub enum TabObProj {
57    /// Projection from tabulator onto source of morphism type.
58    Src(TabMorType),
59
60    /// Projection from tabulator onto target of morphism type.
61    Tgt(TabMorType),
62}
63
64impl TabObProj {
65    /// Morphism type that the tabulator is of.
66    pub fn mor_type(&self) -> &TabMorType {
67        match self {
68            TabObProj::Src(m) | TabObProj::Tgt(m) => m,
69        }
70    }
71}
72
73/// Operation on objects in a discrete tabulator theory.
74pub type TabObOp = Path<TabObType, TabObProj>;
75
76/// Projection onto morphism type in a discrete tabulator theory.
77#[derive(Clone, Debug, PartialEq, Eq)]
78pub enum TabMorProj {
79    /// Projection from a tabulator onto the original morphism type.
80    Cone(TabMorType),
81
82    /// Projection from tabulator onto source of morphism type.
83    Src(TabMorType),
84
85    /// Projection from tabulator onto target of morphism type.
86    Tgt(TabMorType),
87}
88
89impl TabMorProj {
90    /// Morphism type that the tabulator is of.
91    pub fn mor_type(&self) -> &TabMorType {
92        match self {
93            TabMorProj::Cone(m) | TabMorProj::Src(m) | TabMorProj::Tgt(m) => m,
94        }
95    }
96
97    /// Source projection.
98    fn src(self) -> TabObProj {
99        match self {
100            TabMorProj::Cone(m) | TabMorProj::Src(m) => TabObProj::Src(m),
101            TabMorProj::Tgt(m) => TabObProj::Tgt(m),
102        }
103    }
104
105    /// Target projection.
106    fn tgt(self) -> TabObProj {
107        match self {
108            TabMorProj::Src(m) => TabObProj::Src(m),
109            TabMorProj::Cone(m) | TabMorProj::Tgt(m) => TabObProj::Tgt(m),
110        }
111    }
112}
113
114/// Operation on morphisms in a discrete tabulator theory.
115#[derive(Clone, Debug, PartialEq, Eq)]
116pub struct TabMorOp {
117    dom: Path<TabObType, TabMorType>,
118    projections: Vec<TabMorProj>,
119}
120
121/// A discrete tabulator theory.
122///
123/// Loosely speaking, a discrete tabulator theory is a [discrete double
124/// theory](crate::dbl::theory::DiscreteDblTheory) extended to allow tabulators.
125/// That doesn't quite make sense as stated because a
126/// [tabulator](https://ncatlab.org/nlab/show/tabulator) comes with two projection
127/// arrows and a projection cell, which cannot exist in a nontrivial discrete double
128/// category. A **discrete tabulator theory** is thus a small double category with
129/// tabulators and with no arrows or cells beyond the identities and tabulator
130/// projections.
131#[derive(Clone, Default)]
132pub struct DiscreteTabTheory {
133    ob_types: HashFinSet<QualifiedName>,
134    mor_types: HashFinSet<QualifiedName>,
135    src: HashColumn<QualifiedName, TabObType>,
136    tgt: HashColumn<QualifiedName, TabObType>,
137    compose_map: HashColumn<(QualifiedName, QualifiedName), TabMorType>,
138}
139
140impl DiscreteTabTheory {
141    /// Creates an empty discrete tabulator theory.
142    pub fn new() -> Self {
143        Default::default()
144    }
145
146    /// Constructs a tabulator of a morphism type.
147    pub fn tabulator(&self, m: TabMorType) -> TabObType {
148        TabObType::Tabulator(Box::new(m))
149    }
150
151    /// Constructs a unary projection cell for a tabulator.
152    pub fn unary_projection(&self, proj: TabMorProj) -> TabMorOp {
153        TabMorOp {
154            dom: self.unit(self.tabulator(proj.mor_type().clone())).unwrap().into(),
155            projections: vec![proj],
156        }
157    }
158
159    /// Adds a generating object type to the theory.
160    pub fn add_ob_type(&mut self, v: QualifiedName) -> bool {
161        self.ob_types.insert(v)
162    }
163
164    /// Adds a generating morphism type to the theory.
165    pub fn add_mor_type(&mut self, e: QualifiedName, src: TabObType, tgt: TabObType) -> bool {
166        self.src.set(e.clone(), src);
167        self.tgt.set(e.clone(), tgt);
168        self.make_mor_type(e)
169    }
170
171    /// Adds a generating morphim type without initializing its source/target.
172    pub fn make_mor_type(&mut self, e: QualifiedName) -> bool {
173        self.mor_types.insert(e)
174    }
175}
176
177/// Graph of objects and projection arrows in discrete tabulator theory.
178#[derive(RefCast)]
179#[repr(transparent)]
180struct DiscTabTheoryProjGraph(DiscreteTabTheory);
181
182impl Graph for DiscTabTheoryProjGraph {
183    type V = TabObType;
184    type E = TabObProj;
185
186    fn has_vertex(&self, x: &Self::V) -> bool {
187        self.0.has_ob(x)
188    }
189    fn has_edge(&self, proj: &Self::E) -> bool {
190        self.0.has_proarrow(proj.mor_type())
191    }
192
193    fn src(&self, proj: &Self::E) -> Self::V {
194        TabObType::Tabulator(Box::new(proj.mor_type().clone()))
195    }
196    fn tgt(&self, proj: &Self::E) -> Self::V {
197        match proj {
198            TabObProj::Src(m) => self.0.src(m),
199            TabObProj::Tgt(m) => self.0.tgt(m),
200        }
201    }
202}
203
204impl VDblCategory for DiscreteTabTheory {
205    type Ob = TabObType;
206    type Arr = TabObOp;
207    type Pro = TabMorType;
208    type Cell = TabMorOp;
209
210    fn has_ob(&self, ob: &Self::Ob) -> bool {
211        match ob {
212            TabObType::Basic(v) => self.ob_types.contains(v),
213            TabObType::Tabulator(m) => self.has_proarrow(m),
214        }
215    }
216    fn has_arrow(&self, path: &Self::Arr) -> bool {
217        path.contained_in(DiscTabTheoryProjGraph::ref_cast(self))
218    }
219    fn has_proarrow(&self, pro: &Self::Pro) -> bool {
220        match pro {
221            TabMorType::Basic(e) => self.mor_types.contains(e),
222            TabMorType::Hom(x) => self.has_ob(x),
223        }
224    }
225    fn has_cell(&self, cell: &Self::Cell) -> bool {
226        let graph = ProedgeGraph::ref_cast(UnderlyingDblGraph::ref_cast(self));
227        if !cell.dom.contained_in(graph) {
228            return false;
229        }
230        let (src, tgt) = (self.cell_src(cell), self.cell_tgt(cell));
231        self.has_arrow(&src)
232            && self.has_arrow(&tgt)
233            && cell.dom.src(graph) == self.dom(&src)
234            && cell.dom.tgt(graph) == self.dom(&tgt)
235    }
236
237    fn dom(&self, path: &Self::Arr) -> Self::Ob {
238        path.src(DiscTabTheoryProjGraph::ref_cast(self))
239    }
240    fn cod(&self, path: &Self::Arr) -> Self::Ob {
241        path.tgt(DiscTabTheoryProjGraph::ref_cast(self))
242    }
243    fn src(&self, m: &Self::Pro) -> Self::Ob {
244        match m {
245            TabMorType::Basic(e) => {
246                self.src.apply_to_ref(e).expect("Source of morphism type should be defined")
247            }
248            TabMorType::Hom(x) => (**x).clone(),
249        }
250    }
251    fn tgt(&self, m: &Self::Pro) -> Self::Ob {
252        match m {
253            TabMorType::Basic(e) => {
254                self.tgt.apply_to_ref(e).expect("Target of morphism type should be defined")
255            }
256            TabMorType::Hom(x) => (**x).clone(),
257        }
258    }
259
260    fn cell_dom(&self, cell: &Self::Cell) -> Path<Self::Ob, Self::Pro> {
261        cell.dom.clone()
262    }
263    fn cell_cod(&self, cell: &Self::Cell) -> Self::Pro {
264        self.composite(cell.dom.clone()).expect("Path should have a composite")
265    }
266    fn cell_src(&self, cell: &Self::Cell) -> Self::Arr {
267        let graph = ProedgeGraph::ref_cast(UnderlyingDblGraph::ref_cast(self));
268        Path::collect(cell.projections.iter().cloned().map(|proj| proj.src()))
269            .unwrap_or_else(|| Path::empty(cell.dom.src(graph)))
270    }
271    fn cell_tgt(&self, cell: &Self::Cell) -> Self::Arr {
272        let graph = ProedgeGraph::ref_cast(UnderlyingDblGraph::ref_cast(self));
273        Path::collect(cell.projections.iter().cloned().map(|proj| proj.tgt()))
274            .unwrap_or_else(|| Path::empty(cell.dom.tgt(graph)))
275    }
276
277    fn compose(&self, path: Path<Self::Ob, Self::Arr>) -> Self::Arr {
278        path.flatten()
279    }
280
281    fn compose_cells(&self, tree: DblTree<Self::Arr, Self::Pro, Self::Cell>) -> Self::Cell {
282        let graph = UnderlyingDblGraph::ref_cast(self);
283        let dom = tree.dom(graph);
284        let src = self.compose(tree.src(graph));
285        let tgt = self.compose(tree.tgt(graph));
286        assert_eq!(src.len(), tgt.len(), "Source/target boundaries should have equal length");
287        let projections = std::iter::zip(src, tgt)
288            .map(|pair| match pair {
289                (TabObProj::Src(m), TabObProj::Tgt(n)) if m == n => TabMorProj::Cone(m),
290                (TabObProj::Src(m), TabObProj::Src(n)) if m == n => TabMorProj::Src(m),
291                (TabObProj::Tgt(m), TabObProj::Tgt(n)) if m == n => TabMorProj::Tgt(m),
292                _ => panic!("Projection cells should have compatible source/target boundaries"),
293            })
294            .collect();
295        TabMorOp { dom, projections }
296    }
297}
298
299impl VDCWithComposites for DiscreteTabTheory {
300    fn composite2(&self, m: Self::Pro, n: Self::Pro) -> Option<Self::Pro> {
301        let mn = match (m, n) {
302            (m, TabMorType::Hom(y)) if self.tgt(&m) == *y => m,
303            (TabMorType::Hom(x), n) if self.src(&n) == *x => n,
304            (TabMorType::Basic(d), TabMorType::Basic(e)) => {
305                self.compose_map.apply((d, e)).expect("Composition should be defined")
306            }
307            _ => panic!("Ill-typed composite of morphism types in discrete tabulator theory"),
308        };
309        Some(mn)
310    }
311    fn unit(&self, x: Self::Ob) -> Option<Self::Pro> {
312        Some(TabMorType::Hom(Box::new(x)))
313    }
314    fn composite(&self, path: Path<Self::Ob, Self::Pro>) -> Option<Self::Pro> {
315        Some(path.reduce(|x| self.unit(x).unwrap(), |m, n| self.composite2(m, n).unwrap()))
316    }
317
318    fn composite_ext(&self, path: Path<Self::Ob, Self::Pro>) -> Option<Self::Cell> {
319        Some(TabMorOp { dom: path, projections: vec![] })
320    }
321
322    fn through_composite(&self, cell: Self::Cell, range: Range<usize>) -> Option<Self::Cell> {
323        let graph = ProedgeGraph::ref_cast(UnderlyingDblGraph::ref_cast(self));
324        let TabMorOp { dom, projections } = cell;
325        Some(TabMorOp {
326            dom: dom.replace_subpath(graph, range, |sub| self.composite(sub).unwrap().into()),
327            projections,
328        })
329    }
330}
331
332crate::dbl::theory::impl_dbl_theory!(DiscreteTabTheory, crate::dbl::theory::Unital);
333
334#[cfg(test)]
335mod tests {
336    use super::*;
337    use crate::dbl::theory::DblTheory;
338
339    #[test]
340    fn theory_interface() {
341        let mut th = DiscreteTabTheory::new();
342        th.add_ob_type(name("*"));
343        let x = TabObType::Basic(name("*"));
344        assert!(th.has_ob_type(&x));
345        let tab = th.tabulator(th.hom_type(x.clone()));
346        assert!(th.has_ob_type(&tab));
347        assert!(th.has_mor_type(&th.hom_type(tab.clone())));
348
349        th.add_mor_type(name("m"), x.clone(), tab.clone());
350        let m = TabMorType::Basic(name("m"));
351        assert!(th.has_mor_type(&m));
352        assert_eq!(th.src_type(&m), x);
353        assert_eq!(th.tgt_type(&m), tab);
354
355        let proj = th.unary_projection(TabMorProj::Cone(th.hom_type(x.clone())));
356        let cell = th.compose_cells2(
357            [th.composite2_ext(th.hom_type(tab.clone()), th.hom_type(tab.clone())).unwrap()],
358            proj.clone(),
359        );
360        assert!(th.has_mor_op(&cell));
361        assert!(matches!(th.src_op(&cell).only(), Some(TabObProj::Src(_))));
362        assert!(matches!(th.tgt_op(&cell).only(), Some(TabObProj::Tgt(_))));
363
364        let proj_src = th.unary_projection(TabMorProj::Src(th.hom_type(x.clone())));
365        let cell_alt = th.compose_cells2(
366            [proj_src, proj],
367            th.composite2_ext(th.hom_type(x.clone()), th.hom_type(x.clone())).unwrap(),
368        );
369        assert!(th.has_mor_op(&cell_alt));
370        assert_eq!(cell, cell_alt);
371    }
372}
catlog/dbl/discrete_tabulator/theory.rs

catlog/dbl/discrete_tabulator/
theory.rs
