catlog/dbl/modal/
theory.rs

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

catlog/dbl/modal/
theory.rs
