You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
A discrete cartesian theory is a cartesian double theory that is "vertically trivial": its only arrows and cells are structure maps between products. Thus, the vertical structure can be neglected.
Analogous to how a discrete double theory is specified by a category (its category of objects and proarrows), a discrete cartesian theory is specified by a monoidal category. Implement a data structure DiscreteCartesianTheory as a newtype wrapper around a monoidal category.
A discrete cartesian theory is a cartesian double theory that is "vertically trivial": its only arrows and cells are structure maps between products. Thus, the vertical structure can be neglected.
Analogous to how a discrete double theory is specified by a category (its category of objects and proarrows), a discrete cartesian theory is specified by a monoidal category. Implement a data structure
DiscreteCartesianTheory
as a newtype wrapper around a monoidal category.Depends on #242.
The text was updated successfully, but these errors were encountered: