Expand description
A toolbox for categorical logic based on double-categorical theories.
§Organization
While the purpose of this package is to implement double theories and their models and morphisms, a certain amount of lower-dimensional category theory is necessary as background. The package is organized into top-level modules according to dimensionality:
zero: Sets and mappings, known semi-seriously as zero-dimensional category theory, and a bit of abstract algebra.one: Ordinary, or one-dimensional, category theory.dbl: Double category theory.
The prerequisite modules make no pretence to completeness, but if they become sufficiently useful in their own right, they may be spun off into their own crates.
Modules§
- dbl
- Double category theory and two-dimensional categorical logic.
- one
- Category theory in dimension one.
- refs
- References to the literature (docs only).
- simulate
- Simulation of dynamical systems.
- stdlib
- Standard library of double theories, models, and analyses.
- validate
- Objects that can validate themselves.
- zero
- Sets and functions, and a little abstract algebra.