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 std::fmt;
71
72use nonempty::NonEmpty;
73
74use super::graph::InvalidVDblGraph;
75use super::tree::DblTree;
76use crate::one::{InvalidPathEq, Path};
77use crate::zero::QualifiedName;
78
79pub use super::discrete::theory::*;
80pub use super::discrete_tabulator::theory::*;
81pub use super::modal::theory::*;
82
83/// The kind of a double theory, determining whether hom types are guaranteed.
84///
85/// Sealed trait machinery for [`DblTheoryKind`]: prevents external implementors.
86mod private {
87    pub trait Sealed {}
88    impl Sealed for super::Unital {}
89    impl Sealed for super::NonUnital {}
90}
91
92/// This trait uses a generic associated type ([`Wrap`](DblTheoryKind::Wrap)) to
93/// control the return type of [`DblTheory::hom_type`] and
94/// [`DblTheory::hom_op`]. For [`Unital`] theories, `Wrap<T>` is just `T`
95/// (hom types always exist). For [`NonUnital`] theories, `Wrap<T>` is
96/// `Option<T>` (hom types may not exist).
97///
98/// This trait is [sealed] and cannot be implemented outside this crate.
99///
100/// [sealed]: https://rust-lang.github.io/api-guidelines/future-proofing.html#sealed-traits-protect-against-downstream-implementations-c-sealed
101pub trait DblTheoryKind: fmt::Debug + private::Sealed {
102    /// Wraps a type to reflect whether values are guaranteed to exist.
103    ///
104    /// For [`Unital`], this is the identity (`T`).
105    /// For [`NonUnital`], this is `Option<T>`.
106    type Wrap<T>;
107
108    /// Converts from an `Option` into a wrapped value.
109    ///
110    /// For [`Unital`], this unwraps with the given message.
111    /// For [`NonUnital`], this is the identity.
112    fn from_option<T>(opt: Option<T>, msg: &str) -> Self::Wrap<T>;
113}
114
115/// Unital double theories guarantee that every object type has a hom type.
116///
117/// Models of a categorical theory assign *categories* (not just sets) to each
118/// object type: the hom type provides the morphisms.
119#[derive(Clone, Debug, Default)]
120pub struct Unital;
121
122impl DblTheoryKind for Unital {
123    type Wrap<T> = T;
124
125    fn from_option<T>(opt: Option<T>, msg: &str) -> T {
126        opt.expect(msg)
127    }
128}
129
130/// Set-theoretic double theories make no guarantee that hom types exist.
131///
132/// The [`hom_type`](DblTheory::hom_type) method may return `None` for some or
133/// all object types.
134#[derive(Clone, Debug, Default)]
135pub struct NonUnital;
136
137impl DblTheoryKind for NonUnital {
138    type Wrap<T> = Option<T>;
139
140    fn from_option<T>(opt: Option<T>, _msg: &str) -> Option<T> {
141        opt
142    }
143}
144
145/// A double theory.
146///
147/// A double theory is a [virtual double category](super::category) viewed as
148/// specifying a categorical structure. The associated type [`Kind`](DblTheory::Kind)
149/// determines whether hom types are guaranteed to exist ([`Unital`]) or not
150/// ([`NonUnital`]).
151///
152/// See the [module-level docs](super::theory) for background on the terminology.
153pub trait DblTheory {
154    /// The kind of the theory: [`Unital`] or [`NonUnital`].
155    type Kind: DblTheoryKind;
156
157    /// Rust type of object types in the theory.
158    ///
159    /// Viewing the double theory as a virtual double category, this is the type of
160    /// objects.
161    type ObType: Eq + Clone;
162
163    /// Rust type of morphism types in the theory.
164    ///
165    /// Viewing the double theory as a virtual double category, this is the type of
166    /// proarrows.
167    type MorType: Eq + Clone;
168
169    /// Rust type of operations on objects in the double theory.
170    ///
171    /// Viewing the double theory as a virtual double category, this is the type of
172    /// arrows.
173    type ObOp: Eq + Clone;
174
175    /// Rust type of operations on morphisms in the double theory.
176    ///
177    /// Viewing the double theory as a virtual double category, this is the type of
178    /// cells.
179    type MorOp: Eq + Clone;
180
181    /// Does the object type belong to the theory?
182    fn has_ob_type(&self, x: &Self::ObType) -> bool;
183
184    /// Does the morphism type belong to the theory?
185    fn has_mor_type(&self, m: &Self::MorType) -> bool;
186
187    /// Does the object operation belong to the theory?
188    fn has_ob_op(&self, f: &Self::ObOp) -> bool;
189
190    /// Does the morphism operation belong to the theory?
191    fn has_mor_op(&self, α: &Self::MorOp) -> bool;
192
193    /// Source of a morphism type.
194    fn src_type(&self, m: &Self::MorType) -> Self::ObType;
195
196    /// Target of a morphism type.
197    fn tgt_type(&self, m: &Self::MorType) -> Self::ObType;
198
199    /// Domain of an operation on objects.
200    fn ob_op_dom(&self, f: &Self::ObOp) -> Self::ObType;
201
202    /// Codomain of an operation on objects.
203    fn ob_op_cod(&self, f: &Self::ObOp) -> Self::ObType;
204
205    /// Source operation of an operation on morphisms.
206    fn src_op(&self, α: &Self::MorOp) -> Self::ObOp;
207
208    /// Target operation of an operation on morphisms.
209    fn tgt_op(&self, α: &Self::MorOp) -> Self::ObOp;
210
211    /// Domain of an operation on morphisms, a path of morphism types.
212    fn mor_op_dom(&self, α: &Self::MorOp) -> Path<Self::ObType, Self::MorType>;
213
214    /// Codomain of an operation on morphisms, a single morphism type.
215    fn mor_op_cod(&self, α: &Self::MorOp) -> Self::MorType;
216
217    /// Composes a sequence of morphism types, if they have a composite.
218    fn compose_types(&self, path: Path<Self::ObType, Self::MorType>) -> Option<Self::MorType>;
219
220    /// Hom morphism type on an object type.
221    ///
222    /// Viewing the double theory as a virtual double category, this is the unit
223    /// proarrow on an object.
224    ///
225    /// For [`Unital`] theories, this returns `Self::MorType` directly.
226    /// For [`NonUnital`] theories, this returns `Option<Self::MorType>`.
227    fn hom_type(&self, x: Self::ObType) -> <Self::Kind as DblTheoryKind>::Wrap<Self::MorType>;
228
229    /// Compose a sequence of operations on objects.
230    fn compose_ob_ops(&self, path: Path<Self::ObType, Self::ObOp>) -> Self::ObOp;
231
232    /// Identity operation on an object type.
233    ///
234    /// View the double theory as a virtual double category, this is the identity
235    /// arrow on an object.
236    fn id_ob_op(&self, x: Self::ObType) -> Self::ObOp {
237        self.compose_ob_ops(Path::Id(x))
238    }
239
240    /// Hom morphism operation on an object operation.
241    ///
242    /// Viewing the double theory as a virtual double category, this is the unit
243    /// cell on an arrow.
244    ///
245    /// For [`Unital`] theories, this returns `Self::MorOp` directly.
246    /// For [`NonUnital`] theories, this returns `Option<Self::MorOp>`.
247    fn hom_op(&self, f: Self::ObOp) -> <Self::Kind as DblTheoryKind>::Wrap<Self::MorOp>;
248
249    /// Compose operations on morphisms.
250    fn compose_mor_ops(&self, tree: DblTree<Self::ObOp, Self::MorType, Self::MorOp>)
251    -> Self::MorOp;
252
253    /// Identity operation on a morphism type.
254    ///
255    /// Viewing the double theory as a virtual double category, this is the identity
256    /// cell on a proarrow.
257    fn id_mor_op(&self, m: Self::MorType) -> Self::MorOp {
258        self.compose_mor_ops(DblTree::empty(m))
259    }
260}
261
262/// Implements [`DblTheory`] for a type that implements [`VDCWithComposites`].
263///
264/// Two forms are supported:
265///
266/// - `impl_dbl_theory!(Type, Kind)`: for a concrete kind (`Unital` or `NonUnital`).
267/// - `impl_dbl_theory!(Type<Kind>)`: for a type generic over `Kind: DblTheoryKind`,
268///   producing a single generic impl.
269macro_rules! impl_dbl_theory {
270    ($ty:ty, $kind:ty) => {
271        impl $crate::dbl::theory::DblTheory for $ty {
272            type Kind = $kind;
273            $crate::dbl::theory::impl_dbl_theory!(@body);
274        }
275    };
276    ($ty:ident < $kind:ident >) => {
277        impl<$kind: $crate::dbl::theory::DblTheoryKind> $crate::dbl::theory::DblTheory
278            for $ty<$kind>
279        {
280            type Kind = $kind;
281            $crate::dbl::theory::impl_dbl_theory!(@body);
282        }
283    };
284    (@body) => {
285        type ObType = <Self as $crate::dbl::category::VDblCategory>::Ob;
286        type MorType = <Self as $crate::dbl::category::VDblCategory>::Pro;
287        type ObOp = <Self as $crate::dbl::category::VDblCategory>::Arr;
288        type MorOp = <Self as $crate::dbl::category::VDblCategory>::Cell;
289
290        fn has_ob_type(&self, x: &Self::ObType) -> bool {
291            $crate::dbl::category::VDblCategory::has_ob(self, x)
292        }
293        fn has_mor_type(&self, m: &Self::MorType) -> bool {
294            $crate::dbl::category::VDblCategory::has_proarrow(self, m)
295        }
296        fn has_ob_op(&self, f: &Self::ObOp) -> bool {
297            $crate::dbl::category::VDblCategory::has_arrow(self, f)
298        }
299        fn has_mor_op(&self, α: &Self::MorOp) -> bool {
300            $crate::dbl::category::VDblCategory::has_cell(self, α)
301        }
302
303        fn src_type(&self, m: &Self::MorType) -> Self::ObType {
304            $crate::dbl::category::VDblCategory::src(self, m)
305        }
306        fn tgt_type(&self, m: &Self::MorType) -> Self::ObType {
307            $crate::dbl::category::VDblCategory::tgt(self, m)
308        }
309        fn ob_op_dom(&self, f: &Self::ObOp) -> Self::ObType {
310            $crate::dbl::category::VDblCategory::dom(self, f)
311        }
312        fn ob_op_cod(&self, f: &Self::ObOp) -> Self::ObType {
313            $crate::dbl::category::VDblCategory::cod(self, f)
314        }
315
316        fn src_op(&self, α: &Self::MorOp) -> Self::ObOp {
317            $crate::dbl::category::VDblCategory::cell_src(self, α)
318        }
319        fn tgt_op(&self, α: &Self::MorOp) -> Self::ObOp {
320            $crate::dbl::category::VDblCategory::cell_tgt(self, α)
321        }
322        fn mor_op_dom(
323            &self, α: &Self::MorOp,
324        ) -> $crate::one::Path<Self::ObType, Self::MorType> {
325            $crate::dbl::category::VDblCategory::cell_dom(self, α)
326        }
327        fn mor_op_cod(&self, α: &Self::MorOp) -> Self::MorType {
328            $crate::dbl::category::VDblCategory::cell_cod(self, α)
329        }
330
331        fn compose_types(
332            &self,
333            path: $crate::one::Path<Self::ObType, Self::MorType>,
334        ) -> Option<Self::MorType> {
335            $crate::dbl::category::VDCWithComposites::composite(self, path)
336        }
337
338        fn hom_type(
339            &self,
340            x: Self::ObType,
341        ) -> <Self::Kind as $crate::dbl::theory::DblTheoryKind>::Wrap<Self::MorType> {
342            <Self::Kind as $crate::dbl::theory::DblTheoryKind>::from_option(
343                $crate::dbl::category::VDCWithComposites::unit(self, x),
344                "Unital double theory should have all hom types",
345            )
346        }
347        fn hom_op(
348            &self,
349            f: Self::ObOp,
350        ) -> <Self::Kind as $crate::dbl::theory::DblTheoryKind>::Wrap<Self::MorOp> {
351            <Self::Kind as $crate::dbl::theory::DblTheoryKind>::from_option(
352                $crate::dbl::category::VDCWithComposites::unit_arrow(self, f),
353                "Unital double theory should have all hom ops",
354            )
355        }
356
357        fn compose_ob_ops(
358            &self,
359            path: $crate::one::Path<Self::ObType, Self::ObOp>,
360        ) -> Self::ObOp {
361            $crate::dbl::category::VDblCategory::compose(self, path)
362        }
363        fn compose_mor_ops(
364            &self,
365            tree: $crate::dbl::tree::DblTree<Self::ObOp, Self::MorType, Self::MorOp>,
366        ) -> Self::MorOp {
367            $crate::dbl::category::VDblCategory::compose_cells(self, tree)
368        }
369    };
370}
371
372pub(crate) use impl_dbl_theory;
373
374/// A failure of a double theory to be well defined.
375#[derive(Debug, PartialEq, Eq)]
376pub enum InvalidDblTheory {
377    /// Morphism type with an invalid source type.
378    SrcType(QualifiedName),
379
380    /// Morphism type with an invalid target type.
381    TgtType(QualifiedName),
382
383    /// Object operation with an invalid domain.
384    ObOpDom(QualifiedName),
385
386    /// Object operation with an invalid codomain.
387    ObOpCod(QualifiedName),
388
389    /// Morphism operation with an invalid domain.
390    MorOpDom(QualifiedName),
391
392    /// Morphism operation with an invalid codomain.
393    MorOpCod(QualifiedName),
394
395    /// Morphism operation with an invalid source operation.
396    SrcOp(QualifiedName),
397
398    /// Morphism operation with an invalid target operation.
399    TgtOp(QualifiedName),
400
401    /// Morphism operation having a boundary with incompatible corners.
402    MorOpBoundary(QualifiedName),
403
404    /// Equation between morphism types with one or more errors.
405    MorTypeEq(usize, NonEmpty<InvalidPathEq>),
406
407    /// Equation between object operations with one or more errors.
408    ObOpEq(usize, NonEmpty<InvalidPathEq>),
409}
410
411impl From<InvalidVDblGraph<QualifiedName, QualifiedName, QualifiedName>> for InvalidDblTheory {
412    fn from(err: InvalidVDblGraph<QualifiedName, QualifiedName, QualifiedName>) -> Self {
413        match err {
414            InvalidVDblGraph::Dom(id) => InvalidDblTheory::ObOpDom(id),
415            InvalidVDblGraph::Cod(id) => InvalidDblTheory::ObOpCod(id),
416            InvalidVDblGraph::Src(id) => InvalidDblTheory::SrcType(id),
417            InvalidVDblGraph::Tgt(id) => InvalidDblTheory::TgtType(id),
418            InvalidVDblGraph::SquareDom(id) => InvalidDblTheory::MorOpDom(id),
419            InvalidVDblGraph::SquareCod(id) => InvalidDblTheory::MorOpCod(id),
420            InvalidVDblGraph::SquareSrc(id) => InvalidDblTheory::SrcOp(id),
421            InvalidVDblGraph::SquareTgt(id) => InvalidDblTheory::TgtOp(id),
422            InvalidVDblGraph::NotSquare(id) => InvalidDblTheory::MorOpBoundary(id),
423        }
424    }
425}
catlog/dbl/theory.rs

catlog/dbl/
theory.rs
