catlog/dbl/discrete/
theory.rs

1//! Discrete double theories.
2
3use std::ops::Range;
4
5use derive_more::From;
6use ref_cast::RefCast;
7
8use crate::dbl::{category::*, theory::InvalidDblTheory, tree::DblTree};
9use crate::one::{Path, QualifiedPath, category::*, fp_category::*};
10use crate::validate::{self, Validate};
11use crate::zero::QualifiedName;
12
13/// A discrete double theory.
14///
15/// A **discrete double theory** is a double theory with no nontrivial operations on
16/// either object or morphism types. Viewed as a double category, such a theory is
17/// indeed **discrete**, which can equivalently be defined as:
18///
19/// - a discrete object in the 2-category of double categories
20/// - a double category whose underlying categories are both discrete categories
21#[derive(From, RefCast, Debug)]
22#[repr(transparent)]
23pub struct DiscreteDblTheory(pub QualifiedFpCategory);
24
25impl VDblCategory for DiscreteDblTheory {
26    type Ob = QualifiedName;
27    type Arr = QualifiedName;
28    type Pro = QualifiedPath;
29    type Cell = Path<Self::Ob, Self::Pro>;
30
31    fn has_ob(&self, ob: &Self::Ob) -> bool {
32        self.0.has_ob(ob)
33    }
34    fn has_arrow(&self, arr: &Self::Arr) -> bool {
35        self.0.has_ob(arr)
36    }
37    fn has_proarrow(&self, pro: &Self::Pro) -> bool {
38        self.0.has_mor(pro)
39    }
40    fn has_cell(&self, path: &Self::Cell) -> bool {
41        path.contained_in(UnderlyingGraph::ref_cast(&self.0))
42    }
43
44    fn dom(&self, f: &Self::Arr) -> Self::Ob {
45        f.clone()
46    }
47    fn cod(&self, f: &Self::Arr) -> Self::Ob {
48        f.clone()
49    }
50    fn src(&self, m: &Self::Pro) -> Self::Ob {
51        self.0.dom(m)
52    }
53    fn tgt(&self, m: &Self::Pro) -> Self::Ob {
54        self.0.cod(m)
55    }
56
57    fn cell_dom(&self, path: &Self::Cell) -> Path<Self::Ob, Self::Pro> {
58        path.clone()
59    }
60    fn cell_cod(&self, path: &Self::Cell) -> Self::Pro {
61        self.composite(path.clone()).expect("Path should have a composite")
62    }
63    fn cell_src(&self, path: &Self::Cell) -> Self::Arr {
64        path.src(UnderlyingGraph::ref_cast(&self.0))
65    }
66    fn cell_tgt(&self, path: &Self::Cell) -> Self::Arr {
67        path.tgt(UnderlyingGraph::ref_cast(&self.0))
68    }
69
70    fn compose(&self, path: Path<Self::Ob, Self::Arr>) -> Self::Arr {
71        let disc = DiscreteCategory::ref_cast(ObSet::ref_cast(&self.0));
72        disc.compose(path)
73    }
74
75    fn compose_cells(&self, tree: DblTree<Self::Arr, Self::Pro, Self::Cell>) -> Self::Cell {
76        tree.dom(UnderlyingDblGraph::ref_cast(self))
77    }
78}
79
80impl VDCWithComposites for DiscreteDblTheory {
81    fn composite(&self, path: Path<Self::Ob, Self::Pro>) -> Option<Self::Pro> {
82        Some(self.0.compose(path))
83    }
84
85    /// In a discrete double theory, every cell is an extension.
86    fn composite_ext(&self, path: Path<Self::Ob, Self::Pro>) -> Option<Self::Cell> {
87        Some(path)
88    }
89
90    fn through_composite(&self, path: Self::Cell, range: Range<usize>) -> Option<Self::Cell> {
91        let graph = UnderlyingGraph::ref_cast(&self.0);
92        Some(path.replace_subpath(graph, range, |subpath| self.0.compose(subpath).into()))
93    }
94}
95
96crate::dbl::theory::impl_dbl_theory!(DiscreteDblTheory, crate::dbl::theory::Unital);
97
98impl Validate for DiscreteDblTheory {
99    type ValidationError = InvalidDblTheory;
100
101    fn validate(&self) -> Result<(), nonempty::NonEmpty<Self::ValidationError>> {
102        validate::wrap_errors(self.0.iter_invalid().map(|err| match err {
103            InvalidFpCategory::Dom(id) => InvalidDblTheory::SrcType(id),
104            InvalidFpCategory::Cod(id) => InvalidDblTheory::TgtType(id),
105            InvalidFpCategory::Eqn(eq, errs) => InvalidDblTheory::MorTypeEq(eq, errs),
106        }))
107    }
108}
109
110#[cfg(test)]
111mod tests {
112    use super::*;
113    use crate::dbl::theory::DblTheory;
114    use crate::one::{Path, fp_category::FpCategory};
115    use crate::zero::name;
116
117    #[test]
118    fn theory_interface() {
119        let mut sgn = FpCategory::new();
120        sgn.add_ob_generator(name("*"));
121        sgn.add_mor_generator(name("n"), name("*"), name("*"));
122        sgn.equate(Path::pair(name("n"), name("n")), Path::Id(name("*")));
123
124        let th = DiscreteDblTheory::from(sgn);
125        assert!(th.has_ob_type(&name("*")));
126        assert!(th.has_mor_type(&name("n").into()));
127        let path = Path::pair(name("n").into(), name("n").into());
128        assert!(th.0.morphisms_are_equal(th.compose_types(path).unwrap(), Path::Id(name("*"))));
129
130        assert_eq!(th.hom_type(name("*")), Path::Id(name("*")));
131        assert_eq!(th.hom_op(name("*")), Path::single(Path::Id(name("*"))));
132    }
133}
catlog/dbl/discrete/theory.rs

catlog/dbl/discrete/
theory.rs
