catlog/dbl/mod.rs
1//! Double category theory and double-categorical logic.
2//!
3//! # Organization
4//!
5//! This module is the heart of the crate. Its purpose is to implement
6//! double-categorical logic: double theories and their models and morphisms.
7//!
8//! ## Prerequisites
9//!
10//! As prequisites, this module provides some general abstractions from double
11//! category theory:
12//!
13//! - [Virtual double categories](category) (VDCs), our preferred variant of double
14//! categories
15//! - [Virtual double graphs](graph), the data underlying a virtual double category
16//! - [Double trees](tree), the data structure for pasting diagrams in a VDC
17//!
18//! ## Double-categorical logic
19//!
20//! Interfaces are provided for concepts from double-categorical logic:
21//!
22//! - [Double theories](theory), a kind of two-dimensional
23//! [theory](https://ncatlab.org/nlab/show/theory) in the sense of logic
24//! - [Models](model) of double theories, which are categorical structures
25//! - [Morphisms](model_morphism) between models of double theories, generalizing
26//! functors between categories
27//! - [Diagrams](model_diagram) in a model, generalizing
28//! [diagrams](https://ncatlab.org/nlab/show/diagram) in a category
29//!
30//! These submodules mostly provide traits and generic data structures applicable to
31//! any kind of double theory, model, etc. Specific kinds are implemented in the
32//! submodules below and reexported above.
33//!
34//! ## Specific double doctrines
35//!
36//! Just as there are many kinds of one-dimensional theories---algebraic theories,
37//! finite limit theories, regular theories, and so on---so are there many kinds of
38//! double theories. Each such kind we call a "double doctrine". The following
39//! double doctrines are currently implemented, named according to their theories:
40//!
41//! - [Discrete double theories](discrete): double theories with only trivial
42//! operations, and no further structure
43//! - [Discrete tabulator theories](discrete_tabulator): double theories with
44//! tabulators and only trivial operations
45//! - [Modal double theories](modal): double theories equipped with
46//! [modalities][modal::theory::Modality]
47
48pub mod category;
49pub mod computad;
50pub mod graph;
51pub mod tree;
52
53pub mod model;
54pub mod model_diagram;
55pub mod model_instance;
56pub mod model_morphism;
57pub mod theory;
58
59pub mod discrete;
60pub mod discrete_tabulator;
61pub mod modal;
62
63pub use self::category::*;
64pub use self::graph::*;
65pub use self::tree::*;