catlog/dbl/
theory.rs

1/*! Double theories.
2
3A double theory specifies a categorical structure, meaning a category (or
4categories) equipped with extra structure. The spirit of the formalism is that a
5double theory is "just" a [virtual double category](super::category),
6categorifying Lawvere's idea that a theory is "just" a category. Thus, a double
7theory is a [concept with an
8attitude](https://ncatlab.org/nlab/show/concept+with+an+attitude). To bring out
9these intuitions, the interface for double theories, [`DblTheory`], introduces
10new terminology compared to the references cited below.
11
12# Terminology
13
14A double theory comprises four kinds of things:
15
161. **Object type**, interpreted in models as a set of objects.
17
182. **Morphism type**, having a source and a target object type and interpreted
19   in models as a span of morphisms (or
20   [heteromorphisms](https://ncatlab.org/nlab/show/heteromorphism)) between sets
21   of objects.
22
233. **Object operation**, interpreted in models as a function between sets of
24   objects.
25
264. **Morphism operation**, having a source and target object operation and
27   interpreted in models as map between spans of morphisms.
28
29The dictionary between the type-theoretic and double-categorical terminology is
30summarized by the table:
31
32| Associated type                 | Double theory      | Double category           | Interpreted as |
33|---------------------------------|--------------------|---------------------------|----------------|
34| [`ObType`](DblTheory::ObType)   | Object type        | Object                    | Set            |
35| [`MorType`](DblTheory::MorType) | Morphism type      | Proarrow (loose morphism) | Span           |
36| [`ObOp`](DblTheory::ObOp)       | Object operation   | Arrow (tight morphism)    | Function       |
37| [`MorOp`](DblTheory::MorOp)     | Morphism operation | Cell                      | Map of spans   |
38
39Models of a double theory are *categorical* structures, rather than merely
40*set-theoretical* ones, because each object type is assigned not just a set of
41objects but also a span of morphisms between those objects, constituting a
42category. The morphisms come from a distinguished "Hom" morphism type for each
43object type in the double theory. Similarly, each object operation is not just a
44function but a functor because it comes with an "Hom" operation between the Hom
45types. Moreover, morphism types can be composed to give new ones, as summarized
46by the table:
47
48| Method                                      | Double theory          | Double category        |
49|---------------------------------------------|------------------------|------------------------|
50| [`hom_type`](DblTheory::hom_type)           | Hom type               | Identity proarrow      |
51| [`hom_op`](DblTheory::hom_op)               | Hom operation          | Identity cell on arrow |
52| [`compose_types`](DblTheory::compose_types) | Compose morphism types | Compose proarrows      |
53
54Finally, operations on both objects and morphisms have identities and can be
55composed:
56
57| Method                                          | Double theory                       | Double category           |
58|-------------------------------------------------|-------------------------------------|---------------------------|
59| [`id_ob_op`](DblTheory::id_ob_op)               | Identity operation on object type   | Identity arrow            |
60| [`id_mor_op`](DblTheory::id_mor_op)             | Identity operation on morphism type | Identity cell on proarrow |
61| [`compose_ob_ops`](DblTheory::compose_ob_ops)   | Compose object operations           | Compose arrows            |
62| [`compose_mor_ops`](DblTheory::compose_mor_ops) | Compose morphism operations         | Compose cells             |
63
64# References
65
66- [Lambert & Patterson, 2024](crate::refs::CartDblTheories)
67- [Patterson, 2024](crate::refs::DblProducts),
68  Section 10: Finite-product double theories
69*/
70
71use std::hash::{BuildHasher, BuildHasherDefault, Hash, RandomState};
72use std::ops::Range;
73
74use derivative::Derivative;
75use derive_more::From;
76use ref_cast::RefCast;
77use ustr::{IdentityHasher, Ustr};
78
79use super::category::*;
80use super::graph::ProedgeGraph;
81use super::tree::{DblNode, DblTree};
82use crate::one::{Graph, path::Path};
83use crate::one::{category::*, fin_category::UstrFinCategory};
84use crate::validate::Validate;
85use crate::zero::*;
86
87/** A double theory.
88
89A double theory is "just" a virtual double category (VDC) assumed to have units.
90Reflecting this, this trait has a blanket implementation for any
91[`VDblCategory`]. It is not recommended to implement this trait directly.
92
93See the [module-level docs](super::theory) for background on the terminology.
94 */
95pub trait DblTheory {
96    /** Rust type of object types in the theory.
97
98    Viewing the double theory as a virtual double category, this is the type of
99    objects.
100    */
101    type ObType: Eq + Clone;
102
103    /** Rust type of morphism types in the theory.
104
105    Viewing the double theory as a virtual double category, this is the type of
106    proarrows.
107    */
108    type MorType: Eq + Clone;
109
110    /** Rust type of operations on objects in the double theory.
111
112    Viewing the double theory as a virtual double category, this is the type of
113    arrows.
114    */
115    type ObOp: Eq + Clone;
116
117    /** Rust type of operations on morphisms in the double theory.
118
119    Viewing the double theory as a virtual double category, this is the type of
120    cells.
121    */
122    type MorOp: Eq + Clone;
123
124    /// Does the object type belong to the theory?
125    fn has_ob_type(&self, x: &Self::ObType) -> bool;
126
127    /// Does the morphism type belong to the theory?
128    fn has_mor_type(&self, m: &Self::MorType) -> bool;
129
130    /// Does the object operation belong to the theory?
131    fn has_ob_op(&self, f: &Self::ObOp) -> bool;
132
133    /// Does the morphism operation belong to the theory?
134    fn has_mor_op(&self, α: &Self::MorOp) -> bool;
135
136    /// Source of a morphism type.
137    fn src_type(&self, m: &Self::MorType) -> Self::ObType;
138
139    /// Target of a morphism type.
140    fn tgt_type(&self, m: &Self::MorType) -> Self::ObType;
141
142    /// Domain of an operation on objects.
143    fn ob_op_dom(&self, f: &Self::ObOp) -> Self::ObType;
144
145    /// Codomain of an operation on objects.
146    fn ob_op_cod(&self, f: &Self::ObOp) -> Self::ObType;
147
148    /// Source operation of an operation on morphisms.
149    fn src_op(&self, α: &Self::MorOp) -> Self::ObOp;
150
151    /// Target operation of an operation on morphisms.
152    fn tgt_op(&self, α: &Self::MorOp) -> Self::ObOp;
153
154    /// Domain of an operation on morphisms, a path of morphism types.
155    fn mor_op_dom(&self, α: &Self::MorOp) -> Path<Self::ObType, Self::MorType>;
156
157    /// Codomain of an operation on morphisms, a single morphism type.
158    fn mor_op_cod(&self, α: &Self::MorOp) -> Self::MorType;
159
160    /// Composes a sequence of morphism types, if they have a composite.
161    fn compose_types(&self, path: Path<Self::ObType, Self::MorType>) -> Option<Self::MorType>;
162
163    /** Hom morphism type on an object type.
164
165    Viewing the double theory as a virtual double category, this is the unit
166    proarrow on an object.
167    */
168    fn hom_type(&self, x: Self::ObType) -> Self::MorType {
169        self.compose_types(Path::Id(x))
170            .expect("A double theory should have a hom type for each object type")
171    }
172
173    /// Compose a sequence of operations on objects.
174    fn compose_ob_ops(&self, path: Path<Self::ObType, Self::ObOp>) -> Self::ObOp;
175
176    /** Identity operation on an object type.
177
178    View the double theory as a virtual double category, this is the identity
179    arrow on an object.
180    */
181    fn id_ob_op(&self, x: Self::ObType) -> Self::ObOp {
182        self.compose_ob_ops(Path::Id(x))
183    }
184
185    /** Hom morphism operation on an object operation.
186
187    Viewing the double theory as a virtual double category, this is the unit
188    cell on an arrow.
189     */
190    fn hom_op(&self, f: Self::ObOp) -> Self::MorOp;
191
192    /// Compose operations on morphisms.
193    fn compose_mor_ops(&self, tree: DblTree<Self::ObOp, Self::MorType, Self::MorOp>)
194    -> Self::MorOp;
195
196    /** Identity operation on a morphism type.
197
198    Viewing the double theory as a virtual double category, this is the identity
199    cell on a proarrow.
200    */
201    fn id_mor_op(&self, m: Self::MorType) -> Self::MorOp {
202        self.compose_mor_ops(DblTree::empty(m))
203    }
204}
205
206impl<VDC: VDCWithComposites> DblTheory for VDC {
207    type ObType = VDC::Ob;
208    type MorType = VDC::Pro;
209    type ObOp = VDC::Arr;
210    type MorOp = VDC::Cell;
211
212    fn has_ob_type(&self, x: &Self::ObType) -> bool {
213        self.has_ob(x)
214    }
215    fn has_mor_type(&self, m: &Self::MorType) -> bool {
216        self.has_proarrow(m)
217    }
218    fn has_ob_op(&self, f: &Self::ObOp) -> bool {
219        self.has_arrow(f)
220    }
221    fn has_mor_op(&self, α: &Self::MorOp) -> bool {
222        self.has_cell(α)
223    }
224
225    fn src_type(&self, m: &Self::MorType) -> Self::ObType {
226        self.src(m)
227    }
228    fn tgt_type(&self, m: &Self::MorType) -> Self::ObType {
229        self.tgt(m)
230    }
231    fn ob_op_dom(&self, f: &Self::ObOp) -> Self::ObType {
232        self.dom(f)
233    }
234    fn ob_op_cod(&self, f: &Self::ObOp) -> Self::ObType {
235        self.cod(f)
236    }
237
238    fn src_op(&self, α: &Self::MorOp) -> Self::ObOp {
239        self.cell_src(α)
240    }
241    fn tgt_op(&self, α: &Self::MorOp) -> Self::ObOp {
242        self.cell_tgt(α)
243    }
244    fn mor_op_dom(&self, α: &Self::MorOp) -> Path<Self::ObType, Self::MorType> {
245        self.cell_dom(α)
246    }
247    fn mor_op_cod(&self, α: &Self::MorOp) -> Self::MorType {
248        self.cell_cod(α)
249    }
250
251    fn compose_types(&self, path: Path<Self::ObType, Self::MorType>) -> Option<Self::MorType> {
252        self.composite(path)
253    }
254    fn hom_type(&self, x: Self::ObType) -> Self::MorType {
255        self.unit(x).expect("A double theory should have all hom types")
256    }
257    fn hom_op(&self, f: Self::ObOp) -> Self::MorOp {
258        let y = self.cod(&f);
259        let y_ext = self.unit_ext(y).expect("Codomain of arrow should have hom type");
260        let cell = self.compose_cells(
261            DblTree::from_nodes(vec![DblNode::Spine(f), DblNode::Cell(y_ext)]).unwrap(),
262        );
263        self.through_unit(cell, 0).expect("Domain of arrow should have hom type")
264    }
265
266    fn compose_ob_ops(&self, path: Path<Self::ObType, Self::ObOp>) -> Self::ObOp {
267        self.compose(path)
268    }
269    fn id_ob_op(&self, x: Self::ObType) -> Self::ObOp {
270        self.id(x)
271    }
272
273    fn compose_mor_ops(
274        &self,
275        tree: DblTree<Self::ObOp, Self::MorType, Self::MorOp>,
276    ) -> Self::MorOp {
277        self.compose_cells(tree)
278    }
279    fn id_mor_op(&self, m: Self::MorType) -> Self::MorOp {
280        self.id_cell(m)
281    }
282}
283
284/** A discrete double theory.
285
286A **discrete double theory** is a double theory with no nontrivial operations on
287either object or morphism types. Viewed as a double category, such a theory is
288indeed **discrete**, which can equivalently be defined as
289
290- a discrete object in the 2-category of double categories
291- a double category whose underlying categories are both discrete categories
292*/
293#[derive(From, RefCast, Debug)]
294#[repr(transparent)]
295pub struct DiscreteDblTheory<Cat: FgCategory>(Cat);
296
297/// A discrete double theory with keys of type `Ustr`.
298pub type UstrDiscreteDblTheory = DiscreteDblTheory<UstrFinCategory>;
299
300impl<C: FgCategory> VDblCategory for DiscreteDblTheory<C>
301where
302    C::Ob: Clone,
303    C::Mor: Clone,
304{
305    type Ob = C::Ob;
306    type Arr = C::Ob;
307    type Pro = C::Mor;
308    type Cell = Path<C::Ob, C::Mor>;
309
310    fn has_ob(&self, ob: &Self::Ob) -> bool {
311        self.0.has_ob(ob)
312    }
313    fn has_arrow(&self, arr: &Self::Arr) -> bool {
314        self.0.has_ob(arr)
315    }
316    fn has_proarrow(&self, pro: &Self::Pro) -> bool {
317        self.0.has_mor(pro)
318    }
319    fn has_cell(&self, path: &Self::Cell) -> bool {
320        path.contained_in(UnderlyingGraph::ref_cast(&self.0))
321    }
322
323    fn dom(&self, f: &Self::Arr) -> Self::Ob {
324        f.clone()
325    }
326    fn cod(&self, f: &Self::Arr) -> Self::Ob {
327        f.clone()
328    }
329    fn src(&self, m: &Self::Pro) -> Self::Ob {
330        self.0.dom(m)
331    }
332    fn tgt(&self, m: &Self::Pro) -> Self::Ob {
333        self.0.cod(m)
334    }
335
336    fn cell_dom(&self, path: &Self::Cell) -> Path<Self::Ob, Self::Pro> {
337        path.clone()
338    }
339    fn cell_cod(&self, path: &Self::Cell) -> Self::Pro {
340        self.composite(path.clone()).expect("Path should have a composite")
341    }
342    fn cell_src(&self, path: &Self::Cell) -> Self::Arr {
343        path.src(UnderlyingGraph::ref_cast(&self.0))
344    }
345    fn cell_tgt(&self, path: &Self::Cell) -> Self::Arr {
346        path.tgt(UnderlyingGraph::ref_cast(&self.0))
347    }
348
349    fn compose(&self, path: Path<Self::Ob, Self::Arr>) -> Self::Arr {
350        let disc = DiscreteCategory::ref_cast(ObSet::ref_cast(&self.0));
351        disc.compose(path)
352    }
353
354    fn compose_cells(&self, tree: DblTree<Self::Arr, Self::Pro, Self::Cell>) -> Self::Cell {
355        tree.dom(UnderlyingDblGraph::ref_cast(self))
356    }
357}
358
359impl<C: FgCategory> VDCWithComposites for DiscreteDblTheory<C>
360where
361    C::Ob: Clone,
362    C::Mor: Clone,
363{
364    fn composite(&self, path: Path<Self::Ob, Self::Pro>) -> Option<Self::Pro> {
365        Some(self.0.compose(path))
366    }
367
368    /// In a discrete double theory, every cell is an extension.
369    fn composite_ext(&self, path: Path<Self::Ob, Self::Pro>) -> Option<Self::Cell> {
370        Some(path)
371    }
372
373    fn through_composite(&self, path: Self::Cell, range: Range<usize>) -> Option<Self::Cell> {
374        let graph = UnderlyingGraph::ref_cast(&self.0);
375        Some(path.replace_subpath(graph, range, |subpath| self.0.compose(subpath).into()))
376    }
377}
378
379impl<C: FgCategory + Validate> Validate for DiscreteDblTheory<C> {
380    type ValidationError = C::ValidationError;
381
382    fn validate(&self) -> Result<(), nonempty::NonEmpty<Self::ValidationError>> {
383        self.0.validate()
384    }
385}
386
387/// Object type in a discrete tabulator theory.
388#[derive(Clone, Debug, PartialEq, Eq, Hash)]
389pub enum TabObType<V, E> {
390    /// Basic or generating object type.
391    Basic(V),
392
393    /// Tabulator of a morphism type.
394    Tabulator(Box<TabMorType<V, E>>),
395}
396
397/// Morphism type in a discrete tabulator theory.
398#[derive(Clone, Debug, PartialEq, Eq, Hash)]
399pub enum TabMorType<V, E> {
400    /// Basic or generating morphism type.
401    Basic(E),
402
403    /// Hom type on an object type.
404    Hom(Box<TabObType<V, E>>),
405}
406
407/// Projection onto object type in a discrete tabulator theory.
408#[derive(Clone, Debug, PartialEq, Eq)]
409pub enum TabObProj<V, E> {
410    /// Projection from tabulator onto source of morphism type.
411    Src(TabMorType<V, E>),
412
413    /// Projection from tabulator onto target of morphism type.
414    Tgt(TabMorType<V, E>),
415}
416
417impl<V, E> TabObProj<V, E> {
418    /// Morphism type that the tabulator is of.
419    pub fn mor_type(&self) -> &TabMorType<V, E> {
420        match self {
421            TabObProj::Src(m) | TabObProj::Tgt(m) => m,
422        }
423    }
424}
425
426/// Operation on objects in a discrete tabulator theory.
427pub type TabObOp<V, E> = Path<TabObType<V, E>, TabObProj<V, E>>;
428
429/// Projection onto morphism type in a discrete tabulator theory.
430#[derive(Clone, Debug, PartialEq, Eq)]
431pub enum TabMorProj<V, E> {
432    /// Projection from a tabulator onto the original morphism type.
433    Cone(TabMorType<V, E>),
434
435    /// Projection from tabulator onto source of morphism type.
436    Src(TabMorType<V, E>),
437
438    /// Projection from tabulator onto target of morphism type.
439    Tgt(TabMorType<V, E>),
440}
441
442impl<V, E> TabMorProj<V, E> {
443    /// Morphism type that the tabulator is of.
444    pub fn mor_type(&self) -> &TabMorType<V, E> {
445        match self {
446            TabMorProj::Cone(m) | TabMorProj::Src(m) | TabMorProj::Tgt(m) => m,
447        }
448    }
449
450    /// Source projection.
451    fn src(self) -> TabObProj<V, E> {
452        match self {
453            TabMorProj::Cone(m) | TabMorProj::Src(m) => TabObProj::Src(m),
454            TabMorProj::Tgt(m) => TabObProj::Tgt(m),
455        }
456    }
457
458    /// Target projection
459    fn tgt(self) -> TabObProj<V, E> {
460        match self {
461            TabMorProj::Src(m) => TabObProj::Src(m),
462            TabMorProj::Cone(m) | TabMorProj::Tgt(m) => TabObProj::Tgt(m),
463        }
464    }
465}
466
467/// Operation on morphisms in a discrete tabulator theory.
468#[derive(Clone, Debug, PartialEq, Eq)]
469pub struct TabMorOp<V, E> {
470    dom: Path<TabObType<V, E>, TabMorType<V, E>>,
471    projections: Vec<TabMorProj<V, E>>,
472}
473
474/** A discrete tabulator theory.
475
476Loosely speaking, a discrete tabulator theory is a [discrete double
477theory](DiscreteDblTheory) extended to allow tabulators. That doesn't quite make
478sense as stated because a [tabulator](https://ncatlab.org/nlab/show/tabulator)
479comes with two projection arrows and a projection cell, hence cannot exist in a
480nontrivial discrete double category. A **discrete tabulator theory** is rather a
481small double category with tabulators and with no arrows or cells beyond the
482identities and tabulator projections.
483 */
484#[derive(Clone, Derivative)]
485#[derivative(Default(bound = "S: Default"))]
486pub struct DiscreteTabTheory<V, E, S = RandomState> {
487    ob_types: HashFinSet<V, S>,
488    mor_types: HashFinSet<E, S>,
489    src: HashColumn<E, TabObType<V, E>, S>,
490    tgt: HashColumn<E, TabObType<V, E>, S>,
491    compose_map: HashColumn<(E, E), TabMorType<V, E>>,
492}
493
494/// Discrete tabulator theory with names of type `Ustr`.
495pub type UstrDiscreteTabTheory = DiscreteTabTheory<Ustr, Ustr, BuildHasherDefault<IdentityHasher>>;
496
497impl<V, E, S> DiscreteTabTheory<V, E, S>
498where
499    V: Eq + Clone + Hash,
500    E: Eq + Clone + Hash,
501    S: BuildHasher,
502{
503    /// Creates an empty discrete tabulator theory.
504    pub fn new() -> Self
505    where
506        S: Default,
507    {
508        Default::default()
509    }
510
511    /// Constructs a tabulator of a morphism type.
512    pub fn tabulator(&self, m: TabMorType<V, E>) -> TabObType<V, E> {
513        TabObType::Tabulator(Box::new(m))
514    }
515
516    /// Constructs a unary projection cell for a tabulator.
517    pub fn unary_projection(&self, proj: TabMorProj<V, E>) -> TabMorOp<V, E> {
518        TabMorOp {
519            dom: self.hom_type(self.tabulator(proj.mor_type().clone())).into(),
520            projections: vec![proj],
521        }
522    }
523
524    /// Adds a basic object type to the theory.
525    pub fn add_ob_type(&mut self, v: V) -> bool {
526        self.ob_types.insert(v)
527    }
528
529    /// Adds a basic morphism type to the theory.
530    pub fn add_mor_type(&mut self, e: E, src: TabObType<V, E>, tgt: TabObType<V, E>) -> bool {
531        self.src.set(e.clone(), src);
532        self.tgt.set(e.clone(), tgt);
533        self.make_mor_type(e)
534    }
535
536    /// Adds a basic morphim type without initializing its source or target.
537    pub fn make_mor_type(&mut self, e: E) -> bool {
538        self.mor_types.insert(e)
539    }
540}
541
542/// Graph of objects and projection arrows in discrete tabulator theory.
543#[derive(RefCast)]
544#[repr(transparent)]
545struct DiscTabTheoryProjGraph<V, E, S>(DiscreteTabTheory<V, E, S>);
546
547impl<V, E, S> Graph for DiscTabTheoryProjGraph<V, E, S>
548where
549    V: Eq + Clone + Hash,
550    E: Eq + Clone + Hash,
551    S: BuildHasher,
552{
553    type V = TabObType<V, E>;
554    type E = TabObProj<V, E>;
555
556    fn has_vertex(&self, x: &Self::V) -> bool {
557        self.0.has_ob(x)
558    }
559    fn has_edge(&self, proj: &Self::E) -> bool {
560        self.0.has_proarrow(proj.mor_type())
561    }
562
563    fn src(&self, proj: &Self::E) -> Self::V {
564        TabObType::Tabulator(Box::new(proj.mor_type().clone()))
565    }
566    fn tgt(&self, proj: &Self::E) -> Self::V {
567        match proj {
568            TabObProj::Src(m) => self.0.src(m),
569            TabObProj::Tgt(m) => self.0.tgt(m),
570        }
571    }
572}
573
574impl<V, E, S> VDblCategory for DiscreteTabTheory<V, E, S>
575where
576    V: Eq + Clone + Hash,
577    E: Eq + Clone + Hash,
578    S: BuildHasher,
579{
580    type Ob = TabObType<V, E>;
581    type Arr = TabObOp<V, E>;
582    type Pro = TabMorType<V, E>;
583    type Cell = TabMorOp<V, E>;
584
585    fn has_ob(&self, ob: &Self::Ob) -> bool {
586        match ob {
587            TabObType::Basic(v) => self.ob_types.contains(v),
588            TabObType::Tabulator(m) => self.has_proarrow(m),
589        }
590    }
591    fn has_arrow(&self, path: &Self::Arr) -> bool {
592        path.contained_in(DiscTabTheoryProjGraph::ref_cast(self))
593    }
594    fn has_proarrow(&self, pro: &Self::Pro) -> bool {
595        match pro {
596            TabMorType::Basic(e) => self.mor_types.contains(e),
597            TabMorType::Hom(x) => self.has_ob(x),
598        }
599    }
600    fn has_cell(&self, cell: &Self::Cell) -> bool {
601        let graph = ProedgeGraph::ref_cast(UnderlyingDblGraph::ref_cast(self));
602        if !cell.dom.contained_in(graph) {
603            return false;
604        }
605        let (src, tgt) = (self.cell_src(cell), self.cell_tgt(cell));
606        self.has_arrow(&src)
607            && self.has_arrow(&tgt)
608            && cell.dom.src(graph) == self.dom(&src)
609            && cell.dom.tgt(graph) == self.dom(&tgt)
610    }
611
612    fn dom(&self, path: &Self::Arr) -> Self::Ob {
613        path.src(DiscTabTheoryProjGraph::ref_cast(self))
614    }
615    fn cod(&self, path: &Self::Arr) -> Self::Ob {
616        path.tgt(DiscTabTheoryProjGraph::ref_cast(self))
617    }
618    fn src(&self, m: &Self::Pro) -> Self::Ob {
619        match m {
620            TabMorType::Basic(e) => {
621                self.src.apply(e).expect("Source of morphism type should be defined")
622            }
623            TabMorType::Hom(x) => (**x).clone(),
624        }
625    }
626    fn tgt(&self, m: &Self::Pro) -> Self::Ob {
627        match m {
628            TabMorType::Basic(e) => {
629                self.tgt.apply(e).expect("Target of morphism type should be defined")
630            }
631            TabMorType::Hom(x) => (**x).clone(),
632        }
633    }
634
635    fn cell_dom(&self, cell: &Self::Cell) -> Path<Self::Ob, Self::Pro> {
636        cell.dom.clone()
637    }
638    fn cell_cod(&self, cell: &Self::Cell) -> Self::Pro {
639        self.composite(cell.dom.clone()).expect("Path should have a composite")
640    }
641    fn cell_src(&self, cell: &Self::Cell) -> Self::Arr {
642        let graph = ProedgeGraph::ref_cast(UnderlyingDblGraph::ref_cast(self));
643        Path::collect(cell.projections.iter().cloned().map(|proj| proj.src()))
644            .unwrap_or_else(|| Path::empty(cell.dom.src(graph)))
645    }
646    fn cell_tgt(&self, cell: &Self::Cell) -> Self::Arr {
647        let graph = ProedgeGraph::ref_cast(UnderlyingDblGraph::ref_cast(self));
648        Path::collect(cell.projections.iter().cloned().map(|proj| proj.tgt()))
649            .unwrap_or_else(|| Path::empty(cell.dom.tgt(graph)))
650    }
651
652    fn compose(&self, path: Path<Self::Ob, Self::Arr>) -> Self::Arr {
653        path.flatten()
654    }
655
656    fn compose_cells(&self, tree: DblTree<Self::Arr, Self::Pro, Self::Cell>) -> Self::Cell {
657        let graph = UnderlyingDblGraph::ref_cast(self);
658        let dom = tree.dom(graph);
659        let src = self.compose(tree.src(graph));
660        let tgt = self.compose(tree.tgt(graph));
661        assert_eq!(src.len(), tgt.len(), "Source/target boundaries should have equal length");
662        let projections = std::iter::zip(src, tgt)
663            .map(|pair| match pair {
664                (TabObProj::Src(m), TabObProj::Tgt(n)) if m == n => TabMorProj::Cone(m),
665                (TabObProj::Src(m), TabObProj::Src(n)) if m == n => TabMorProj::Src(m),
666                (TabObProj::Tgt(m), TabObProj::Tgt(n)) if m == n => TabMorProj::Tgt(m),
667                _ => panic!("Projection cells should have compatible source/target boundaries"),
668            })
669            .collect();
670        TabMorOp { dom, projections }
671    }
672}
673
674impl<V, E, S> VDCWithComposites for DiscreteTabTheory<V, E, S>
675where
676    V: Eq + Clone + Hash,
677    E: Eq + Clone + Hash,
678    S: BuildHasher,
679{
680    fn composite2(&self, m: Self::Pro, n: Self::Pro) -> Option<Self::Pro> {
681        let mn = match (m, n) {
682            (m, TabMorType::Hom(y)) if self.tgt(&m) == *y => m,
683            (TabMorType::Hom(x), n) if self.src(&n) == *x => n,
684            (TabMorType::Basic(d), TabMorType::Basic(e)) => {
685                self.compose_map.apply(&(d, e)).expect("Composition should be defined")
686            }
687            _ => panic!("Ill-typed composite of morphism types in discrete tabulator theory"),
688        };
689        Some(mn)
690    }
691    fn unit(&self, x: Self::Ob) -> Option<Self::Pro> {
692        Some(TabMorType::Hom(Box::new(x)))
693    }
694    fn composite(&self, path: Path<Self::Ob, Self::Pro>) -> Option<Self::Pro> {
695        Some(path.reduce(|x| self.unit(x).unwrap(), |m, n| self.composite2(m, n).unwrap()))
696    }
697
698    fn composite_ext(&self, path: Path<Self::Ob, Self::Pro>) -> Option<Self::Cell> {
699        Some(TabMorOp {
700            dom: path,
701            projections: vec![],
702        })
703    }
704
705    fn through_composite(&self, cell: Self::Cell, range: Range<usize>) -> Option<Self::Cell> {
706        let graph = ProedgeGraph::ref_cast(UnderlyingDblGraph::ref_cast(self));
707        let TabMorOp { dom, projections } = cell;
708        Some(TabMorOp {
709            dom: dom.replace_subpath(graph, range, |sub| self.composite(sub).unwrap().into()),
710            projections,
711        })
712    }
713}
714
715#[cfg(test)]
716mod tests {
717    use super::*;
718    use crate::one::fin_category::*;
719
720    #[test]
721    fn discrete_double_theory() {
722        type Mor<V, E> = FinMor<V, E>;
723
724        let mut sgn: FinCategory<char, char> = Default::default();
725        sgn.add_ob_generator('*');
726        sgn.add_mor_generator('n', '*', '*');
727        sgn.set_composite('n', 'n', Mor::Id('*'));
728
729        let th = DiscreteDblTheory::from(sgn);
730        assert!(th.has_ob_type(&'*'));
731        assert!(th.has_mor_type(&Mor::Generator('n')));
732        let path = Path::pair(Mor::Generator('n'), Mor::Generator('n'));
733        assert_eq!(th.compose_types(path), Some(Mor::Id('*')));
734
735        assert_eq!(th.hom_type('*'), Mor::Id('*'));
736        assert_eq!(th.hom_op('*'), Path::single(Mor::Id('*')));
737    }
738
739    #[test]
740    fn discrete_tabulator_theory() {
741        let mut th = DiscreteTabTheory::<char, char>::new();
742        th.add_ob_type('*');
743        let x = TabObType::Basic('*');
744        assert!(th.has_ob_type(&x));
745        let tab = th.tabulator(th.hom_type(x.clone()));
746        assert!(th.has_ob_type(&tab));
747        assert!(th.has_mor_type(&th.hom_type(tab.clone())));
748
749        th.add_mor_type('m', x.clone(), tab.clone());
750        let m = TabMorType::Basic('m');
751        assert!(th.has_mor_type(&m));
752        assert_eq!(th.src_type(&m), x);
753        assert_eq!(th.tgt_type(&m), tab);
754
755        let proj = th.unary_projection(TabMorProj::Cone(th.hom_type(x.clone())));
756        let cell = th.compose_cells2(
757            [th.composite2_ext(th.hom_type(tab.clone()), th.hom_type(tab.clone())).unwrap()],
758            proj.clone(),
759        );
760        assert!(th.has_mor_op(&cell));
761        assert!(matches!(th.src_op(&cell).only(), Some(TabObProj::Src(_))));
762        assert!(matches!(th.tgt_op(&cell).only(), Some(TabObProj::Tgt(_))));
763
764        let proj_src = th.unary_projection(TabMorProj::Src(th.hom_type(x.clone())));
765        let cell_alt = th.compose_cells2(
766            [proj_src, proj],
767            th.composite2_ext(th.hom_type(x.clone()), th.hom_type(x.clone())).unwrap(),
768        );
769        assert!(th.has_mor_op(&cell_alt));
770        assert_eq!(cell, cell_alt);
771    }
772}
catlog/dbl/theory.rs

catlog/dbl/
theory.rs
