Module dbl

Double category theory and double-categorical logic.

Organization

This module is the heart of the crate. Its purpose is to implement double-categorical logic: double theories and their models and morphisms.

Prerequisites

As prequisites, this module provides some general abstractions from double category theory:

• Virtual double categories (VDCs), our preferred variant of double categories
• Virtual double graphs, the data underlying a virtual double category
• Double trees, the data structure for pasting diagrams in a VDC

Double-categorical logic

Interfaces are provided for concepts from double-categorical logic:

• Double theories, a kind of two-dimensional theory in the sense of logic
• Models of double theories, which are categorical structures
• Morphisms between models of double theories, generalizing functors between categories
• Diagrams in a model, generalizing diagrams in a category

These submodules mostly provide traits and generic data structures applicable to any kind of double theory, model, etc. Specific kinds are implemented in the submodules below and reexported above.

Specific double doctrines

Just as there are many kinds of one-dimensional theories—algebraic theories, finite limit theories, regular theories, and so on—so are there many kinds of double theories. Each such kind we call a “double doctrine”. The following double doctrines are currently implemented, named according to their theories:

• Discrete double theories: double theories with only trivial operations, and no further structure
• Discrete tabulator theories: double theories with tabulators and only trivial operations
• Modal double theories: double theories equipped with modalities

Re-exports

pub use self::category::*;

pub use self::graph::*;

pub use self::tree::*;

Modules

category

Virtual double categories.

computad

Computads for virtual double categories.

discrete

Doctrine of discrete double theories.

discrete_tabulator

Doctrine of discrete tabulator theories.

graph

Virtual double graphs.

modal

Doctrine of modal double theories.

model

Models of double theories.

model_diagram

Diagrams in models of a double theory.

model_morphism

Morphisms between models of double theories.

theory

Double theories.

tree

Double trees: pasting diagrams in virtual double categories.