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

catlog/dbl/discrete/
theory.rs
