Function th_category_with_scalars

pub fn th_category_with_scalars() -> UstrDiscreteDblTheory

The theory of categories with scalars.

A category with scalars is a category sliced over the monoid representing a walking idempotent. The morphisms over the identity are interpreted as scalars, which are closed under composition, as are the non-scalar morphisms.

The main intended application is to categories enriched in M-sets for a monoid M such as the positive real numbers under multiplication, but to remain within simple theories the theory defined here is more general.