catlog/dbl/
model_morphism.rs

1//! Morphisms between models of double theories.
2//!
3//! A morphism between [models](super::model) consists of functions between objects
4//! and between morphisms that are:
5//!
6//! 1. *Well-typed*: preserve object and morphism types
7//! 2. *Functorial*: preserve composition and identities
8//! 3. *Natural*: commute with object operations and morphism operations, possibly up
9//!    to comparison maps
10//!
11//! In mathematical terms, a model morphism is a natural transformation between lax
12//! double functors. The natural transformation can be strict, pseudo, lax, or
13//! oplax. For models of *discrete* double theories, all these options coincide.
14//!
15//! # References
16//!
17//! - [Paré 2011](crate::refs::DblYonedaTheory), Section 1.5: Natural
18//!   transformations
19//! - [Lambert & Patterson 2024](crate::refs::CartDblTheories),
20//!   Section 7: Lax transformations
21
22use thiserror::Error;
23
24#[cfg(feature = "serde")]
25use serde::{Deserialize, Serialize};
26#[cfg(feature = "serde-wasm")]
27use tsify::Tsify;
28
29pub use super::discrete::model_morphism::*;
30
31/// An invalid assignment in a morphism between models of a double theory.
32#[derive(Clone, Debug, Error, PartialEq, Eq)]
33#[cfg_attr(feature = "serde", derive(Serialize, Deserialize))]
34#[cfg_attr(feature = "serde", serde(tag = "tag", content = "content"))]
35#[cfg_attr(feature = "serde-wasm", derive(Tsify))]
36#[cfg_attr(feature = "serde-wasm", tsify(into_wasm_abi, from_wasm_abi))]
37pub enum InvalidDblModelMorphism<ObGen, MorGen> {
38    /// An object generator not mapped to an object in the codomain model.
39    #[error("Object generator `{0}` is not mapped to an object in the codomain")]
40    Ob(ObGen),
41
42    /// A morphism generator not mapped to a morphism in the codomain model.
43    #[error("Morphism generator `{0}` is not mapped to a morphism in the codomain")]
44    Mor(MorGen),
45
46    /// A morphism generator whose domain is not preserved.
47    #[error("Domain of morphism generator `{0}` is not preserved")]
48    Dom(MorGen),
49
50    /// A morphism generator whose codomain is not preserved.
51    #[error("Codomain of morphism generator `{0}` is not preserved")]
52    Cod(MorGen),
53
54    /// An object generator whose type is not preserved.
55    #[error("Object `{0}` is not mapped to an object of the same type in the codomain")]
56    ObType(ObGen),
57
58    /// A morphism generator whose type is not preserved.
59    #[error("Morphism `{0}` is not mapped to a morphism of the same type in the codomain")]
60    MorType(MorGen),
61
62    /// A path equation in domain presentation that is not respected.
63    #[error("Path equation `{0}` is not respected")]
64    Eq(usize),
65}
catlog/dbl/model_morphism.rs

catlog/dbl/
model_morphism.rs
