catlog/dbl/modal/
theory.rs

1/*! Modal double theories.
2
3A **modal double theory** is a unital VDC equipped a family of modalities. A
4**modality** is minimally an endomorphism, and is usually a monad or comonad, in
5the 2-category of unital VDCs, normal functors, and natural transformations. In
6a model of a modal double theory, each endomorphism on the theory is interpreted
7as a endofunctor on the VDC of sets, i.e., as a lax double endofunctor on the
8double category of sets. The modalities on the semantics side are fixed across
9all models and include the double list monads and its many variants.
10
11The various modalities are implicitly organized by a **mode theory** ([Licata &
12Shulman 2015](crate::refs::AdjointLogic)), a 2-category whose objects are called
13**modes**, morphisms are called **modalities**, and cells are sometimes called
14**laws**. Our mode theory has only one mode, corresponding to the fact our
15semantics is currently fixed to be the double category of sets and spans. Thus,
16our mode theory is actually a monoidal category. It seems excessively meta at
17this stage to reify the mode theory as the data of a finitely presented
182-category or monoidal category. Instead, the mode theory is implicit and baked
19in at the type level.
20*/
21
22use std::hash::{BuildHasher, BuildHasherDefault, Hash, RandomState};
23use std::iter::repeat_n;
24
25use derive_more::From;
26use ref_cast::RefCast;
27use ustr::{IdentityHasher, Ustr};
28
29use crate::dbl::computad::{AVDCComputad, AVDCComputadTop};
30use crate::dbl::theory::InvalidDblTheory;
31use crate::dbl::{DblTree, InvalidVDblGraph, VDCWithComposites, VDblCategory, VDblGraph};
32use crate::one::computad::{Computad, ComputadTop};
33use crate::validate::{self, Validate};
34use crate::{one::*, zero::*};
35
36/// Modalities available in a modal double theory.
37#[derive(Clone, Copy, Debug, PartialEq, Eq, From)]
38pub enum Modality {
39    /// List modalities, all of which are monads.
40    #[from]
41    List(List),
42
43    /// Discrete modality, an idempotent comonad.
44    Discrete(),
45
46    /// Codiscrete modality, an idempotent monad.
47    Codiscrete(),
48}
49
50/** List modalities available in a modal double theory.
51
52There is just one list, or free monoid, monad on the category of sets, but the
53double category of sets admits, besides the [plain](Self::Plain) list double
54monad, a number of variations decorating the spans of lists with extra
55combinatorial data.
56 */
57#[derive(Clone, Copy, Debug, PartialEq, Eq)]
58pub enum List {
59    /// Lists of objects and morphisms (of same length).
60    Plain,
61
62    /// Lists of objects and morphisms, allowing permutation of the codomain list.
63    Symmetric,
64
65    /** Lists of objects and morphisms, allowing reindexing of the codomain list.
66
67    This modality is a skeletized version of the "finite family", or free finite
68    [coproduct completion](https://ncatlab.org/nlab/show/free+coproduct+completion),
69    construction.
70     */
71    Coproduct,
72
73    /** Lists of objects and morphisms, allowing reindexing of the domain list.
74
75    This modality is a skeletized version of the free finite product completion.
76     */
77    Product,
78
79    /** Lists of objects and morphisms, allowing independent reindexing of both
80    domain and codomain lists.
81
82    This modality is a version of the free finite biproduct completion,
83    equivalent to freely enriching in commutative monoids and then applying the
84    matrix construction (Mac Lane, Exercise VIII.2.6) on such an enriched
85    category.
86    */
87    Biproduct,
88}
89
90/** Application of modalities.
91
92Due to the simplicity of this logic, we can easily put terms in normal form:
93every term is a single argument along with a (possibly empty) list of modalities
94applied to it.
95 */
96#[derive(Clone, Debug, PartialEq, Eq)]
97pub struct ModeApp<T> {
98    /// Argument to which the modalities are applied.
99    pub arg: T,
100
101    /// List of modalities applied (from left to right).
102    pub modalities: Vec<Modality>,
103}
104
105impl<T> ModeApp<T> {
106    /// Constructs a new term with no modalities applied.
107    pub fn new(arg: T) -> Self {
108        Self {
109            arg,
110            modalities: Default::default(),
111        }
112    }
113
114    /** Converts from `&ModeApp<T>` to `ModeApp<&T>`.
115
116    Note that this requires cloning the list of applied modalities.
117    */
118    pub fn as_ref(&self) -> ModeApp<&T> {
119        ModeApp {
120            arg: &self.arg,
121            modalities: self.modalities.clone(),
122        }
123    }
124
125    /// Applies a modality.
126    pub fn apply(mut self, m: Modality) -> Self {
127        self.modalities.push(m);
128        self
129    }
130
131    /// Applies a sequence of modalities.
132    pub fn apply_all(mut self, iter: impl IntoIterator<Item = Modality>) -> Self {
133        self.modalities.extend(iter);
134        self
135    }
136
137    /// Maps over the argument.
138    pub fn map<S, F: FnOnce(T) -> S>(self, f: F) -> ModeApp<S> {
139        let ModeApp { arg, modalities } = self;
140        ModeApp {
141            arg: f(arg),
142            modalities,
143        }
144    }
145
146    /// Maps over the argument, flattening nested applications.
147    pub fn flat_map<S, F: FnOnce(T) -> ModeApp<S>>(self, f: F) -> ModeApp<S> {
148        let ModeApp { arg, modalities } = self;
149        f(arg).apply_all(modalities)
150    }
151}
152
153/** A basic operation in a modal double theory.
154
155These are (object or morphisms) operations that cannot be built out of others
156using the structure of a VDC or virtual equipment.
157 */
158#[derive(Clone, Debug, PartialEq, Eq, From)]
159pub enum ModalOp<Id> {
160    /// Generating operation.
161    #[from]
162    Generator(Id),
163
164    /** List concentation.
165
166    This is a component of the monad multiplication for a [list](List) modality.
167    It is given in unbiased style, where the second argument is the arity.
168     */
169    Concat(List, usize, ModeApp<Id>),
170}
171
172/// An object type in a modal double theory.
173pub type ModalObType<Id> = ModeApp<Id>;
174
175/// A morphism type in a modal double theory.
176pub type ModalMorType<Id> = ShortPath<ModalObType<Id>, ModeApp<Id>>;
177
178impl<Id> ModalMorType<Id> {
179    /// Applies a modality.
180    pub fn apply(self, m: Modality) -> Self {
181        self.map(|x| x.apply(m), |f| f.apply(m))
182    }
183
184    /// Applies a sequence of modalities.
185    pub fn apply_all(self, iter: impl IntoIterator<Item = Modality>) -> Self {
186        match self {
187            ShortPath::Zero(x) => ShortPath::Zero(x.apply_all(iter)),
188            ShortPath::One(f) => ShortPath::One(f.apply_all(iter)),
189        }
190    }
191}
192
193/// An object operation in a modal double theory.
194pub type ModalObOp<Id> = Path<ModalObType<Id>, ModeApp<ModalOp<Id>>>;
195
196impl<Id> ModalObOp<Id> {
197    /// Constructs the object operation for a generator.
198    pub fn generator(id: Id) -> Self {
199        ModeApp::new(ModalOp::Generator(id)).into()
200    }
201
202    /// Constructs a concatenation operation for a list modality.
203    pub fn concat(list: List, arity: usize, ob_type: ModalObType<Id>) -> Self {
204        ModeApp::new(ModalOp::Concat(list, arity, ob_type)).into()
205    }
206
207    fn apply_all(self, iter: impl IntoIterator<Item = Modality> + Clone) -> Self {
208        match self {
209            Path::Id(x) => Path::Id(x.apply_all(iter)),
210            Path::Seq(edges) => Path::Seq(edges.map(|p| p.apply_all(iter.clone()))),
211        }
212    }
213}
214
215/** A node in a morphism operation of a modal double theory.
216
217A generic [morphism operation](ModalMorOp) in a modal double theory is a [double
218tree](DblTree) built out of these nodes.
219 */
220#[derive(Clone, Debug, PartialEq, Eq, From)]
221pub enum ModalNode<Id> {
222    /// Basic morphism operation.
223    #[from]
224    Basic(ModeApp<ModalOp<Id>>),
225
226    /// Unit cell on a basic object operation.
227    Unit(ModeApp<ModalOp<Id>>),
228
229    /** Cell witnessing a composite.
230
231    By assumption, modalities preserve all composites in the theory.
232     */
233    Composite(Path<ModalObType<Id>, ModalMorType<Id>>),
234}
235
236/// A morphism operation in a modal double theory.
237pub type ModalMorOp<Id> = DblTree<ModalObOp<Id>, ModalMorType<Id>, ModalNode<Id>>;
238
239/// A modal double theory.
240#[derive(Debug, Default)]
241pub struct ModalDblTheory<Id, S = RandomState> {
242    ob_generators: HashFinSet<Id, S>,
243    arr_generators: ComputadTop<ModalObType<Id>, Id, S>,
244    pro_generators: ComputadTop<ModalObType<Id>, Id, S>,
245    cell_generators: AVDCComputadTop<ModalObType<Id>, ModalObOp<Id>, ModalMorType<Id>, Id, S>,
246    arr_equations: Vec<PathEq<ModalObType<Id>, ModeApp<ModalOp<Id>>>>,
247    // TODO: Cell equations and composites
248}
249
250/// A modal double theory with identifiers of type `Ustr`.
251pub type UstrModalDblTheory = ModalDblTheory<Ustr, BuildHasherDefault<IdentityHasher>>;
252
253/// Set of object types in a modal double theory.
254#[derive(RefCast)]
255#[repr(transparent)]
256pub(super) struct ModalObTypes<Id, S>(ModalDblTheory<Id, S>);
257
258impl<Id, S> Set for ModalObTypes<Id, S>
259where
260    Id: Eq + Clone + Hash,
261    S: BuildHasher,
262{
263    type Elem = ModeApp<Id>;
264
265    fn contains(&self, ob: &Self::Elem) -> bool {
266        self.0.ob_generators.contains(&ob.arg)
267    }
268}
269
270/// Graph of object types and *basic* morphism types in a modal double theory.
271#[derive(RefCast)]
272#[repr(transparent)]
273struct ModalProedgeGraph<Id, S>(ModalDblTheory<Id, S>);
274
275impl<Id, S> Graph for ModalProedgeGraph<Id, S>
276where
277    Id: Eq + Clone + Hash,
278    S: BuildHasher,
279{
280    type V = ModalObType<Id>;
281    type E = ModeApp<Id>;
282
283    fn has_vertex(&self, ob: &Self::V) -> bool {
284        self.0.loose_computad().has_vertex(ob)
285    }
286    fn has_edge(&self, proedge: &Self::E) -> bool {
287        self.0.loose_computad().has_edge(&proedge.arg)
288    }
289    fn src(&self, proedge: &Self::E) -> Self::V {
290        proedge.as_ref().flat_map(|e| self.0.loose_computad().src(e))
291    }
292    fn tgt(&self, proedge: &Self::E) -> Self::V {
293        proedge.as_ref().flat_map(|e| self.0.loose_computad().tgt(e))
294    }
295}
296
297/// Graph of object/morphism types in a modal double theory.
298#[derive(RefCast)]
299#[repr(transparent)]
300pub(super) struct ModalMorTypeGraph<Id, S>(ModalDblTheory<Id, S>);
301
302impl<Id, S> Graph for ModalMorTypeGraph<Id, S>
303where
304    Id: Eq + Clone + Hash,
305    S: BuildHasher,
306{
307    type V = ModalObType<Id>;
308    type E = ModalMorType<Id>;
309
310    fn has_vertex(&self, x: &Self::V) -> bool {
311        ModalProedgeGraph::ref_cast(&self.0).has_vertex(x)
312    }
313    fn has_edge(&self, path: &Self::E) -> bool {
314        path.contained_in(ModalProedgeGraph::ref_cast(&self.0))
315    }
316    fn src(&self, path: &Self::E) -> Self::V {
317        path.src(ModalProedgeGraph::ref_cast(&self.0))
318    }
319    fn tgt(&self, path: &Self::E) -> Self::V {
320        path.tgt(ModalProedgeGraph::ref_cast(&self.0))
321    }
322}
323
324impl<Id, S> ReflexiveGraph for ModalMorTypeGraph<Id, S>
325where
326    Id: Eq + Clone + Hash,
327    S: BuildHasher,
328{
329    fn refl(&self, x: Self::V) -> Self::E {
330        ShortPath::Zero(x)
331    }
332}
333
334/// Graph of object types and *basic* object operations in a modal theory.
335#[derive(RefCast)]
336#[repr(transparent)]
337struct ModalEdgeGraph<Id, S>(ModalDblTheory<Id, S>);
338
339impl<Id, S> Graph for ModalEdgeGraph<Id, S>
340where
341    Id: Eq + Clone + Hash,
342    S: BuildHasher,
343{
344    type V = ModalObType<Id>;
345    type E = ModeApp<ModalOp<Id>>;
346
347    fn has_vertex(&self, ob: &Self::V) -> bool {
348        self.0.tight_computad().has_vertex(ob)
349    }
350    fn has_edge(&self, edge: &Self::E) -> bool {
351        match &edge.arg {
352            ModalOp::Generator(e) => self.0.tight_computad().has_edge(e),
353            ModalOp::Concat(_, _, ob) => self.0.tight_computad().has_vertex(ob),
354        }
355    }
356    fn src(&self, edge: &Self::E) -> Self::V {
357        edge.as_ref().flat_map(|arg| match arg {
358            ModalOp::Generator(e) => self.0.tight_computad().src(e),
359            ModalOp::Concat(list, n, ob) => {
360                ob.clone().apply_all(repeat_n(Modality::List(*list), *n))
361            }
362        })
363    }
364    fn tgt(&self, edge: &Self::E) -> Self::V {
365        edge.as_ref().flat_map(|arg| match arg {
366            ModalOp::Generator(e) => self.0.tight_computad().tgt(e),
367            ModalOp::Concat(list, _, ob) => ob.clone().apply(Modality::List(*list)),
368        })
369    }
370}
371
372/// Category of object types/operations in a modal double theory.
373#[derive(RefCast)]
374#[repr(transparent)]
375pub(super) struct ModalOneTheory<Id, S>(ModalDblTheory<Id, S>);
376
377impl<Id, S> Category for ModalOneTheory<Id, S>
378where
379    Id: Eq + Clone + Hash,
380    S: BuildHasher,
381{
382    type Ob = ModalObType<Id>;
383    type Mor = ModalObOp<Id>;
384
385    fn has_ob(&self, x: &Self::Ob) -> bool {
386        ModalEdgeGraph::ref_cast(&self.0).has_vertex(x)
387    }
388    fn has_mor(&self, path: &Self::Mor) -> bool {
389        path.contained_in(ModalEdgeGraph::ref_cast(&self.0))
390    }
391    fn dom(&self, path: &Self::Mor) -> Self::Ob {
392        path.src(ModalEdgeGraph::ref_cast(&self.0))
393    }
394    fn cod(&self, path: &Self::Mor) -> Self::Ob {
395        path.tgt(ModalEdgeGraph::ref_cast(&self.0))
396    }
397    fn compose(&self, path: Path<Self::Ob, Self::Mor>) -> Self::Mor {
398        path.flatten()
399    }
400}
401
402/// Virtual double graph of *basic* cells in a modal double theory.
403#[derive(RefCast)]
404#[repr(transparent)]
405struct ModalVDblGraph<Id, S>(ModalDblTheory<Id, S>);
406
407type ModalVDblComputad<'a, Id, S> = AVDCComputad<
408    'a,
409    ModalObType<Id>,
410    ModalObOp<Id>,
411    ModalMorType<Id>,
412    ModalObTypes<Id, S>,
413    UnderlyingGraph<ModalOneTheory<Id, S>>,
414    ModalMorTypeGraph<Id, S>,
415    Id,
416    S,
417>;
418
419impl<Id, S> Validate for ModalVDblGraph<Id, S>
420where
421    Id: Eq + Clone + Hash,
422    S: BuildHasher,
423{
424    type ValidationError = InvalidVDblGraph<Id, Id, Id>;
425
426    fn validate(&self) -> Result<(), nonempty::NonEmpty<Self::ValidationError>> {
427        let edge_cptd = self.0.tight_computad();
428        let edge_errors = edge_cptd.iter_invalid().map(|err| match err {
429            InvalidGraph::Src(e) => InvalidVDblGraph::Dom(e),
430            InvalidGraph::Tgt(e) => InvalidVDblGraph::Cod(e),
431        });
432        let proedge_cptd = self.0.loose_computad();
433        let proedge_errors = proedge_cptd.iter_invalid().map(|err| match err {
434            InvalidGraph::Src(p) => InvalidVDblGraph::Src(p),
435            InvalidGraph::Tgt(p) => InvalidVDblGraph::Tgt(p),
436        });
437        // Make sure one-dimensional data is valid before validating squares.
438        validate::wrap_errors(edge_errors.chain(proedge_errors))?;
439
440        validate::wrap_errors(self.0.dbl_computad().iter_invalid())
441    }
442}
443
444impl<Id, S> VDblGraph for ModalVDblGraph<Id, S>
445where
446    Id: Eq + Clone + Hash,
447    S: BuildHasher,
448{
449    type V = ModalObType<Id>;
450    type E = ModalObOp<Id>;
451    type ProE = ModalMorType<Id>;
452    type Sq = ModalNode<Id>;
453
454    fn has_vertex(&self, x: &Self::V) -> bool {
455        ModalObTypes::ref_cast(&self.0).contains(x)
456    }
457    fn has_edge(&self, path: &Self::E) -> bool {
458        ModalOneTheory::ref_cast(&self.0).has_mor(path)
459    }
460    fn has_proedge(&self, path: &Self::ProE) -> bool {
461        ModalMorTypeGraph::ref_cast(&self.0).has_edge(path)
462    }
463    fn has_square(&self, node: &Self::Sq) -> bool {
464        match node {
465            ModalNode::Basic(app) => match &app.arg {
466                ModalOp::Generator(sq) => self.0.dbl_computad().has_square(sq),
467                ModalOp::Concat(_, _, p) => ModalProedgeGraph::ref_cast(&self.0).has_edge(p),
468            },
469            ModalNode::Unit(f) => ModalEdgeGraph::ref_cast(&self.0).has_edge(f),
470            // FIXME: Don't assume all composites exist.
471            ModalNode::Composite(_) => true,
472        }
473    }
474
475    fn dom(&self, path: &Self::E) -> Self::V {
476        ModalOneTheory::ref_cast(&self.0).dom(path)
477    }
478    fn cod(&self, path: &Self::E) -> Self::V {
479        ModalOneTheory::ref_cast(&self.0).cod(path)
480    }
481    fn src(&self, path: &Self::ProE) -> Self::V {
482        ModalMorTypeGraph::ref_cast(&self.0).src(path)
483    }
484    fn tgt(&self, path: &Self::ProE) -> Self::V {
485        ModalMorTypeGraph::ref_cast(&self.0).tgt(path)
486    }
487
488    fn square_dom(&self, node: &Self::Sq) -> Path<Self::V, Self::ProE> {
489        match node {
490            ModalNode::Basic(app) => {
491                let ModeApp { arg, modalities } = app;
492                let dom = match &arg {
493                    ModalOp::Generator(sq) => self.0.dbl_computad().square_dom(sq),
494                    ModalOp::Concat(list, n, p) => {
495                        let ob_type = p.clone().apply_all(repeat_n(Modality::List(*list), *n));
496                        ShortPath::One(ob_type).into()
497                    }
498                };
499                dom.map(|x| x.apply_all(modalities.clone()), |p| p.apply_all(modalities.clone()))
500            }
501            ModalNode::Unit(f) => {
502                ModalMorType::Zero(ModalEdgeGraph::ref_cast(&self.0).src(f)).into()
503            }
504            ModalNode::Composite(path) => path.clone(),
505        }
506    }
507    fn square_cod(&self, node: &Self::Sq) -> Self::ProE {
508        match node {
509            ModalNode::Basic(app) => {
510                let cod = match &app.arg {
511                    ModalOp::Generator(sq) => self.0.dbl_computad().square_cod(sq),
512                    ModalOp::Concat(list, _, p) => p.clone().apply(Modality::List(*list)).into(),
513                };
514                cod.apply_all(app.modalities.clone())
515            }
516            ModalNode::Unit(f) => ModalMorType::Zero(ModalEdgeGraph::ref_cast(&self.0).tgt(f)),
517            ModalNode::Composite(path) => {
518                self.0.composite(path.clone()).expect("Composite should exist")
519            }
520        }
521    }
522    fn square_src(&self, node: &Self::Sq) -> Self::E {
523        match node {
524            ModalNode::Basic(app) => {
525                let src = match &app.arg {
526                    ModalOp::Generator(sq) => self.0.dbl_computad().square_src(sq),
527                    ModalOp::Concat(list, n, p) => {
528                        let graph = ModalProedgeGraph::ref_cast(&self.0);
529                        ModeApp::new(ModalOp::Concat(*list, *n, graph.src(p))).into()
530                    }
531                };
532                src.apply_all(app.modalities.clone())
533            }
534            ModalNode::Unit(f) => f.clone().into(),
535            ModalNode::Composite(path) => {
536                Path::empty(path.src(ModalMorTypeGraph::ref_cast(&self.0)))
537            }
538        }
539    }
540    fn square_tgt(&self, node: &Self::Sq) -> Self::E {
541        match node {
542            ModalNode::Basic(app) => {
543                let tgt = match &app.arg {
544                    ModalOp::Generator(sq) => self.0.dbl_computad().square_tgt(sq),
545                    ModalOp::Concat(list, n, p) => {
546                        let graph = ModalProedgeGraph::ref_cast(&self.0);
547                        ModeApp::new(ModalOp::Concat(*list, *n, graph.tgt(p))).into()
548                    }
549                };
550                tgt.apply_all(app.modalities.clone())
551            }
552            ModalNode::Unit(f) => f.clone().into(),
553            ModalNode::Composite(path) => {
554                Path::empty(path.tgt(ModalMorTypeGraph::ref_cast(&self.0)))
555            }
556        }
557    }
558    fn arity(&self, node: &Self::Sq) -> usize {
559        match node {
560            ModalNode::Basic(app) => match &app.arg {
561                ModalOp::Generator(sq) => self.0.dbl_computad().arity(sq),
562                ModalOp::Concat(_, _, _) => 1,
563            },
564            ModalNode::Unit(_) => 1,
565            ModalNode::Composite(path) => path.len(),
566        }
567    }
568}
569
570impl<Id, S> VDblCategory for ModalDblTheory<Id, S>
571where
572    Id: Eq + Clone + Hash,
573    S: BuildHasher,
574{
575    type Ob = ModalObType<Id>;
576    type Arr = ModalObOp<Id>;
577    type Pro = ModalMorType<Id>;
578    type Cell = ModalMorOp<Id>;
579
580    fn has_ob(&self, x: &Self::Ob) -> bool {
581        ModalVDblGraph::ref_cast(self).has_vertex(x)
582    }
583    fn has_arrow(&self, f: &Self::Arr) -> bool {
584        ModalVDblGraph::ref_cast(self).has_edge(f)
585    }
586    fn has_proarrow(&self, m: &Self::Pro) -> bool {
587        ModalVDblGraph::ref_cast(self).has_proedge(m)
588    }
589    fn has_cell(&self, tree: &Self::Cell) -> bool {
590        tree.contained_in(ModalVDblGraph::ref_cast(self))
591    }
592
593    fn dom(&self, f: &Self::Arr) -> Self::Ob {
594        ModalVDblGraph::ref_cast(self).dom(f)
595    }
596    fn cod(&self, f: &Self::Arr) -> Self::Ob {
597        ModalVDblGraph::ref_cast(self).cod(f)
598    }
599    fn src(&self, m: &Self::Pro) -> Self::Ob {
600        ModalVDblGraph::ref_cast(self).src(m)
601    }
602    fn tgt(&self, m: &Self::Pro) -> Self::Ob {
603        ModalVDblGraph::ref_cast(self).tgt(m)
604    }
605
606    fn cell_dom(&self, tree: &Self::Cell) -> Path<Self::Ob, Self::Pro> {
607        tree.dom(ModalVDblGraph::ref_cast(self))
608    }
609    fn cell_cod(&self, tree: &Self::Cell) -> Self::Pro {
610        tree.cod(ModalVDblGraph::ref_cast(self))
611    }
612    fn cell_src(&self, tree: &Self::Cell) -> Self::Arr {
613        self.compose(tree.src(ModalVDblGraph::ref_cast(self)))
614    }
615    fn cell_tgt(&self, tree: &Self::Cell) -> Self::Arr {
616        self.compose(tree.tgt(ModalVDblGraph::ref_cast(self)))
617    }
618    fn arity(&self, tree: &Self::Cell) -> usize {
619        tree.arity(ModalVDblGraph::ref_cast(self))
620    }
621
622    fn compose(&self, path: Path<Self::Ob, Self::Arr>) -> Self::Arr {
623        ModalOneTheory::ref_cast(self).compose(path)
624    }
625    fn compose_cells(&self, tree: DblTree<Self::Arr, Self::Pro, Self::Cell>) -> Self::Cell {
626        tree.flatten()
627    }
628}
629
630impl<Id, S> VDCWithComposites for ModalDblTheory<Id, S>
631where
632    Id: Eq + Clone + Hash,
633    S: BuildHasher,
634{
635    fn composite_ext(&self, path: Path<Self::Ob, Self::Pro>) -> Option<Self::Cell> {
636        if self.composite(path.clone()).is_some() {
637            let graph = ModalVDblGraph::ref_cast(self);
638            Some(DblTree::single(ModalNode::Composite(path), graph))
639        } else {
640            None
641        }
642    }
643
644    fn composite(&self, path: Path<Self::Ob, Self::Pro>) -> Option<Self::Pro> {
645        match path {
646            Path::Id(x) => Some(ShortPath::Zero(x)),
647            Path::Seq(ms) => {
648                if ms.len() == 1 {
649                    Some(ms.head)
650                } else {
651                    // TODO: Support nontrivial composites.
652                    None
653                }
654            }
655        }
656    }
657
658    fn through_composite(
659        &self,
660        _cell: Self::Cell,
661        _range: std::ops::Range<usize>,
662    ) -> Option<Self::Cell> {
663        panic!("Universal property of composites is not implemented")
664    }
665}
666
667impl<Id, S> Validate for ModalDblTheory<Id, S>
668where
669    Id: Eq + Clone + Hash,
670    S: BuildHasher,
671{
672    type ValidationError = InvalidDblTheory<Id>;
673
674    fn validate(&self) -> Result<(), nonempty::NonEmpty<Self::ValidationError>> {
675        // Validate generating data.
676        ModalVDblGraph::ref_cast(self)
677            .validate()
678            .map_err(|errs| errs.map(|err| err.into()))?;
679
680        // Validate equations between object operations.
681        let graph = ModalEdgeGraph::ref_cast(self);
682        let arr_errors = self.arr_equations.iter().enumerate().filter_map(|(id, eq)| {
683            let errs = eq.validate_in(graph).err()?;
684            Some(InvalidDblTheory::ObOpEq(id, errs))
685        });
686        validate::wrap_errors(arr_errors)
687    }
688}
689
690impl<Id, S> ModalDblTheory<Id, S>
691where
692    Id: Eq + Clone + Hash,
693    S: BuildHasher,
694{
695    /// Gets the computad generating the proarrows of the theory.
696    pub(super) fn loose_computad(
697        &self,
698    ) -> Computad<'_, ModalObType<Id>, ModalObTypes<Id, S>, Id, S> {
699        Computad::new(ModalObTypes::ref_cast(self), &self.pro_generators)
700    }
701
702    /// Gets the computad generating the arrows of the theory.
703    pub(super) fn tight_computad(
704        &self,
705    ) -> Computad<'_, ModalObType<Id>, ModalObTypes<Id, S>, Id, S> {
706        Computad::new(ModalObTypes::ref_cast(self), &self.arr_generators)
707    }
708
709    /// Gets the double computad generating the theory.
710    pub(super) fn dbl_computad(&self) -> ModalVDblComputad<'_, Id, S> {
711        AVDCComputad::new(
712            ModalObTypes::ref_cast(self),
713            UnderlyingGraph::ref_cast(ModalOneTheory::ref_cast(self)),
714            ModalMorTypeGraph::ref_cast(self),
715            &self.cell_generators,
716        )
717    }
718
719    /// Adds a generating object type to the theory.
720    pub fn add_ob_type(&mut self, id: Id) {
721        self.ob_generators.insert(id);
722    }
723
724    /// Adds a generating morphism type to the theory.
725    pub fn add_mor_type(&mut self, id: Id, src: ModalObType<Id>, tgt: ModalObType<Id>) {
726        self.pro_generators.add_edge(id, src, tgt);
727    }
728
729    /// Adds a generating object operation to the theory.
730    pub fn add_ob_op(&mut self, id: Id, dom: ModalObType<Id>, cod: ModalObType<Id>) {
731        self.arr_generators.add_edge(id, dom, cod);
732    }
733
734    /// Adds a generating morphism operation to the theory.
735    pub fn add_mor_op(
736        &mut self,
737        id: Id,
738        dom: Path<ModalObType<Id>, ModalMorType<Id>>,
739        cod: ModalMorType<Id>,
740        src: ModalObOp<Id>,
741        tgt: ModalObOp<Id>,
742    ) {
743        self.cell_generators.add_square(id, dom, cod.into(), src, tgt);
744    }
745
746    /// Adds a morphism operation with nullary domain and unit codomain.
747    pub fn add_special_mor_op(&mut self, id: Id, src: ModalObOp<Id>, tgt: ModalObOp<Id>) {
748        let dom = self.dom(&src); // == self.dom(&tgt)
749        let cod = self.cod(&src); // == self.cod(&tgt)
750        self.add_mor_op(id, Path::empty(dom), ShortPath::Zero(cod), src, tgt);
751    }
752
753    /// Equate two object operations in the theory.
754    pub fn equate_ob_ops(&mut self, lhs: ModalObOp<Id>, rhs: ModalObOp<Id>) {
755        self.arr_equations.push(PathEq::new(lhs, rhs))
756    }
757}
catlog/dbl/modal/theory.rs

catlog/dbl/modal/
theory.rs
