catlog/dbl/
theory.rs

1//! Double theories.
2//!
3//! A double theory specifies a categorical structure, meaning a category (or
4//! categories) equipped with extra structure. The spirit of the formalism is that a
5//! double theory is "just" a [virtual double category](super::category),
6//! categorifying Lawvere's idea that a theory is "just" a category. Thus, a double
7//! theory is a [concept with an
8//! attitude](https://ncatlab.org/nlab/show/concept+with+an+attitude). To bring out
9//! these intuitions, the interface for double theories, [`DblTheory`], introduces
10//! new terminology compared to the references cited below.
11//!
12//! # Terminology
13//!
14//! A double theory comprises four kinds of things:
15//!
16//! 1. **Object type**, interpreted in models as a set of objects.
17//!
18//! 2. **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//!
23//! 3. **Object operation**, interpreted in models as a function between sets of
24//!    objects.
25//!
26//! 4. **Morphism operation**, having a source and target object operation and
27//!    interpreted in models as map between spans of morphisms.
28//!
29//! The dictionary between the type-theoretic and double-categorical terminology is
30//! summarized 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//!
39//! Models 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
41//! objects but also a span of morphisms between those objects, constituting a
42//! category. The morphisms come from a distinguished "Hom" morphism type for each
43//! object type in the double theory. Similarly, each object operation is not just a
44//! function but a functor because it comes with an "Hom" operation between the Hom
45//! types. Moreover, morphism types can be composed to give new ones, as summarized
46//! by 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//!
54//! Finally, operations on both objects and morphisms have identities and can be
55//! composed:
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
70use nonempty::NonEmpty;
71
72use super::{category::*, graph::InvalidVDblGraph, tree::*};
73use crate::one::{InvalidPathEq, Path, tree::OpenTree};
74use crate::zero::QualifiedName;
75
76pub use super::discrete::theory::*;
77pub use super::discrete_tabulator::theory::*;
78pub use super::modal::theory::*;
79
80/// A double theory.
81///
82/// A double theory is "just" a virtual double category (VDC) assumed to have units.
83/// Reflecting this, this trait has a blanket implementation for any
84/// [`VDblCategory`]. It is not recommended to implement this trait directly.
85///
86/// See the [module-level docs](super::theory) for background on the terminology.
87pub trait DblTheory {
88    /// Rust type of object types in the theory.
89    ///
90    /// Viewing the double theory as a virtual double category, this is the type of
91    /// objects.
92    type ObType: Eq + Clone;
93
94    /// Rust type of morphism types in the theory.
95    ///
96    /// Viewing the double theory as a virtual double category, this is the type of
97    /// proarrows.
98    type MorType: Eq + Clone;
99
100    /// Rust type of operations on objects in the double theory.
101    ///
102    /// Viewing the double theory as a virtual double category, this is the type of
103    /// arrows.
104    type ObOp: Eq + Clone;
105
106    /// Rust type of operations on morphisms in the double theory.
107    ///
108    /// Viewing the double theory as a virtual double category, this is the type of
109    /// cells.
110    type MorOp: Eq + Clone;
111
112    /// Does the object type belong to the theory?
113    fn has_ob_type(&self, x: &Self::ObType) -> bool;
114
115    /// Does the morphism type belong to the theory?
116    fn has_mor_type(&self, m: &Self::MorType) -> bool;
117
118    /// Does the object operation belong to the theory?
119    fn has_ob_op(&self, f: &Self::ObOp) -> bool;
120
121    /// Does the morphism operation belong to the theory?
122    fn has_mor_op(&self, α: &Self::MorOp) -> bool;
123
124    /// Source of a morphism type.
125    fn src_type(&self, m: &Self::MorType) -> Self::ObType;
126
127    /// Target of a morphism type.
128    fn tgt_type(&self, m: &Self::MorType) -> Self::ObType;
129
130    /// Domain of an operation on objects.
131    fn ob_op_dom(&self, f: &Self::ObOp) -> Self::ObType;
132
133    /// Codomain of an operation on objects.
134    fn ob_op_cod(&self, f: &Self::ObOp) -> Self::ObType;
135
136    /// Source operation of an operation on morphisms.
137    fn src_op(&self, α: &Self::MorOp) -> Self::ObOp;
138
139    /// Target operation of an operation on morphisms.
140    fn tgt_op(&self, α: &Self::MorOp) -> Self::ObOp;
141
142    /// Domain of an operation on morphisms, a path of morphism types.
143    fn mor_op_dom(&self, α: &Self::MorOp) -> Path<Self::ObType, Self::MorType>;
144
145    /// Codomain of an operation on morphisms, a single morphism type.
146    fn mor_op_cod(&self, α: &Self::MorOp) -> Self::MorType;
147
148    /// Composes a sequence of morphism types, if they have a composite.
149    fn compose_types(&self, path: Path<Self::ObType, Self::MorType>) -> Option<Self::MorType>;
150
151    /// Hom morphism type on an object type.
152    ///
153    /// Viewing the double theory as a virtual double category, this is the unit
154    /// proarrow on an object.
155    fn hom_type(&self, x: Self::ObType) -> Self::MorType {
156        self.compose_types(Path::Id(x))
157            .expect("A double theory should have a hom type for each object type")
158    }
159
160    /// Compose a sequence of operations on objects.
161    fn compose_ob_ops(&self, path: Path<Self::ObType, Self::ObOp>) -> Self::ObOp;
162
163    /// Identity operation on an object type.
164    ///
165    /// View the double theory as a virtual double category, this is the identity
166    /// arrow on an object.
167    fn id_ob_op(&self, x: Self::ObType) -> Self::ObOp {
168        self.compose_ob_ops(Path::Id(x))
169    }
170
171    /// Hom morphism operation on an object operation.
172    ///
173    /// Viewing the double theory as a virtual double category, this is the unit
174    /// cell on an arrow.
175    fn hom_op(&self, f: Self::ObOp) -> Self::MorOp;
176
177    /// Compose operations on morphisms.
178    fn compose_mor_ops(&self, tree: DblTree<Self::ObOp, Self::MorType, Self::MorOp>)
179    -> Self::MorOp;
180
181    /// Identity operation on a morphism type.
182    ///
183    /// Viewing the double theory as a virtual double category, this is the identity
184    /// cell on a proarrow.
185    fn id_mor_op(&self, m: Self::MorType) -> Self::MorOp {
186        self.compose_mor_ops(DblTree::empty(m))
187    }
188}
189
190impl<VDC: VDCWithComposites> DblTheory for VDC {
191    type ObType = VDC::Ob;
192    type MorType = VDC::Pro;
193    type ObOp = VDC::Arr;
194    type MorOp = VDC::Cell;
195
196    fn has_ob_type(&self, x: &Self::ObType) -> bool {
197        self.has_ob(x)
198    }
199    fn has_mor_type(&self, m: &Self::MorType) -> bool {
200        self.has_proarrow(m)
201    }
202    fn has_ob_op(&self, f: &Self::ObOp) -> bool {
203        self.has_arrow(f)
204    }
205    fn has_mor_op(&self, α: &Self::MorOp) -> bool {
206        self.has_cell(α)
207    }
208
209    fn src_type(&self, m: &Self::MorType) -> Self::ObType {
210        self.src(m)
211    }
212    fn tgt_type(&self, m: &Self::MorType) -> Self::ObType {
213        self.tgt(m)
214    }
215    fn ob_op_dom(&self, f: &Self::ObOp) -> Self::ObType {
216        self.dom(f)
217    }
218    fn ob_op_cod(&self, f: &Self::ObOp) -> Self::ObType {
219        self.cod(f)
220    }
221
222    fn src_op(&self, α: &Self::MorOp) -> Self::ObOp {
223        self.cell_src(α)
224    }
225    fn tgt_op(&self, α: &Self::MorOp) -> Self::ObOp {
226        self.cell_tgt(α)
227    }
228    fn mor_op_dom(&self, α: &Self::MorOp) -> Path<Self::ObType, Self::MorType> {
229        self.cell_dom(α)
230    }
231    fn mor_op_cod(&self, α: &Self::MorOp) -> Self::MorType {
232        self.cell_cod(α)
233    }
234
235    fn compose_types(&self, path: Path<Self::ObType, Self::MorType>) -> Option<Self::MorType> {
236        self.composite(path)
237    }
238    fn hom_type(&self, x: Self::ObType) -> Self::MorType {
239        self.unit(x).expect("A double theory should have all hom types")
240    }
241    fn hom_op(&self, f: Self::ObOp) -> Self::MorOp {
242        let y = self.cod(&f);
243        let y_ext = self.unit_ext(y).expect("Codomain of arrow should have hom type");
244        let cell = self.compose_cells(DblTree(
245            OpenTree::linear(vec![DblNode::Spine(f), DblNode::Cell(y_ext)]).unwrap(),
246        ));
247        self.through_unit(cell, 0).expect("Domain of arrow should have hom type")
248    }
249
250    fn compose_ob_ops(&self, path: Path<Self::ObType, Self::ObOp>) -> Self::ObOp {
251        self.compose(path)
252    }
253    fn id_ob_op(&self, x: Self::ObType) -> Self::ObOp {
254        self.id(x)
255    }
256
257    fn compose_mor_ops(
258        &self,
259        tree: DblTree<Self::ObOp, Self::MorType, Self::MorOp>,
260    ) -> Self::MorOp {
261        self.compose_cells(tree)
262    }
263    fn id_mor_op(&self, m: Self::MorType) -> Self::MorOp {
264        self.id_cell(m)
265    }
266}
267
268/// A failure of a double theory to be well defined.
269#[derive(Debug)]
270pub enum InvalidDblTheory {
271    /// Morphism type with an invalid source type.
272    SrcType(QualifiedName),
273
274    /// Morphism type with an invalid target type.
275    TgtType(QualifiedName),
276
277    /// Object operation with an invalid domain.
278    ObOpDom(QualifiedName),
279
280    /// Object operation with an invalid codomain.
281    ObOpCod(QualifiedName),
282
283    /// Morphism operation with an invalid domain.
284    MorOpDom(QualifiedName),
285
286    /// Morphism operation with an invalid codomain.
287    MorOpCod(QualifiedName),
288
289    /// Morphism operation with an invalid source operation.
290    SrcOp(QualifiedName),
291
292    /// Morphism operation with an invalid target operation.
293    TgtOp(QualifiedName),
294
295    /// Morphism operation having a boundary with incompatible corners.
296    MorOpBoundary(QualifiedName),
297
298    /// Equation between morphism types with one or more errors.
299    MorTypeEq(usize, NonEmpty<InvalidPathEq>),
300
301    /// Equation between object operations with one or more errors.
302    ObOpEq(usize, NonEmpty<InvalidPathEq>),
303}
304
305impl From<InvalidVDblGraph<QualifiedName, QualifiedName, QualifiedName>> for InvalidDblTheory {
306    fn from(err: InvalidVDblGraph<QualifiedName, QualifiedName, QualifiedName>) -> Self {
307        match err {
308            InvalidVDblGraph::Dom(id) => InvalidDblTheory::ObOpDom(id),
309            InvalidVDblGraph::Cod(id) => InvalidDblTheory::ObOpCod(id),
310            InvalidVDblGraph::Src(id) => InvalidDblTheory::SrcType(id),
311            InvalidVDblGraph::Tgt(id) => InvalidDblTheory::TgtType(id),
312            InvalidVDblGraph::SquareDom(id) => InvalidDblTheory::MorOpDom(id),
313            InvalidVDblGraph::SquareCod(id) => InvalidDblTheory::MorOpCod(id),
314            InvalidVDblGraph::SquareSrc(id) => InvalidDblTheory::SrcOp(id),
315            InvalidVDblGraph::SquareTgt(id) => InvalidDblTheory::TgtOp(id),
316            InvalidVDblGraph::NotSquare(id) => InvalidDblTheory::MorOpBoundary(id),
317        }
318    }
319}
catlog/dbl/theory.rs

catlog/dbl/
theory.rs
