Module theory 

Double theories as used by DoubleTT.

In catlog, double theories belonging to different double doctrines (discrete theories, modal theories, etc) are represented using different data structures. By contrast, there is just one implementation of DoubleTT, intended to support all of the features that we need. To provide a uniform interface to theories of different doctrines, theories are boxed in an enum (TheoryDef). This design is similar to that taken in catlog-wasm.

Structs

Theory

A theory supported by DoubleTT, comprising a name and a definition.

Enums

MorType

Morphism type in a double theory supported by DoubleTT.

ObOp

Object operation in a double theory supported by DoubleTT.

ObType

Object type in a double theory supported by DoubleTT.

TheoryDef

Definition of a double theory supported by DoubleTT.

Functions

std_theories

Construct a library of standard theories.