Standard library of theories

Catlab's standard library of generalized algebraic theories.

The focus is on categories and monoidal categories, but other related structures are also included.

Syntax for a free cartesian category.

In this syntax, the pairing and projection operations are defined using duplication and deletion, and do not have their own syntactic elements. This convention could be dropped or reversed.

Syntax for a free cartesian closed category.

See also FreeCartesianCategory.

Syntax for a 2-category.

Checks domains of morphisms but not 2-morphisms.

Syntax for a free closed monoidal category.

Syntax for a free cocartesian category.

In this syntax, the copairing and inclusion operations are defined using merging and creation, and do not have their own syntactic elements. This convention could be dropped or reversed.

Theory of abelian bicategories of relations

Unlike BicategoryRelations, this theory uses additive notation.

References:

• Carboni & Walters, 1987, "Cartesian bicategories I", Sec. 5
• Baez & Erbele, 2015, "Categories in control"

Theory of bicategories of relations

TODO: The 2-morphisms are missing.

References:

• Carboni & Walters, 1987, "Cartesian bicategories I"
• Walters, 2009, blog post, "Categorical algebras of relations", http://rfcwalters.blogspot.com/2009/10/categorical-algebras-of-relations.html

Theory of biproduct categories

Mathematically the same as SemiadditiveCategory but written multiplicatively, instead of additively.

Theory of cartesian (monoidal) categories

For the traditional axiomatization of products, see CategoryWithProducts.

Theory of cartesian closed categories, aka CCCs

A CCC is a cartesian category with internal homs (aka, exponential objects).

FIXME: This theory should also extend ClosedMonoidalCategory, but multiple inheritance is not yet supported.

Theory of categories (with no extra structure)

Warning: We compose functions from left to right, i.e., if f:A→B and g:B→C then compose(f,g):A→C. Under this convention function are applied on the right, e.g., if a∈A then af∈B.

We retain the usual meaning of the symbol ∘ (\circ), i.e., g∘f = compose(f,g). This usage is too entrenched to overturn, inconvenient though it may be. We use symbol ⋅ (\cdot) for diagrammatic composition: f⋅g = compose(f,g).

Theory of (strict) 2-categories

Theory of a category with (finite) coproducts

Finite coproducts are presented in biased style, via the nullary case (initial objects) and the binary case (binary coproducts). The axioms are dual to those of CategoryWithProducts.

For a monoidal category axiomatization, see CocartesianCategory.

Theory of a category with (finite) products

Finite products are presented in biased style, via the nullary case (terminal objects) and the binary case (binary products). The equational axioms are standard, especially in type theory (Lambek & Scott, 1986, Section 0.5 or Section I.3). Strictly speaking, this theory is not of a "category with finite products" (a category in which finite products exist) but of a "category with chosen finite products".

For a monoidal category axiomatization, see CartesianCategory.

Theory of (symmetric) closed monoidal categories

Theory of cocartesian (monoidal) categories

For the traditional axiomatization of coproducts, see CategoryWithCoproducts.

Theory of a (finitely) cocomplete category

Finite colimits are presented in biased style, via finite coproducts and coequalizers. The axioms are dual to those of CompleteCategory.

Theory of compact closed categories

Theory of a (finitely) complete category

Finite limits are presented in biased style, via finite products and equalizers. The equational axioms for equalizers are obscure, but can found in (Lambek & Scott, 1986, Section 0.5), which follow "Burroni's pioneering ideas". Strictly speaking, this theory is not of a "finitely complete category" (a category in which finite limits exist) but of a "category with chosen finite limits".

Theory of dagger categories

Theory of dagger compact categories

In a dagger compact category, there are two kinds of adjoints of a morphism f::Hom(A,B), the adjoint mate mate(f)::Hom(dual(B),dual(A)) and the dagger adjoint dagger(f)::Hom(B,A). In the category of Hilbert spaces, these are respectively the Banach space adjoint and the Hilbert space adjoint (Reed-Simon, Vol I, Sec VI.2). In Julia, they would correspond to transpose and adjoint in the official LinearAlegbra module. For the general relationship between mates and daggers, see Selinger's survey of graphical languages for monoidal categories.

FIXME: This theory should also extend DaggerCategory, but multiple inheritance is not yet supported.

Theory of dagger symmetric monoidal categories

Also known as a symmetric monoidal dagger category.

FIXME: This theory should also extend DaggerCategory, but multiple inheritance is not yet supported.

Theory of a distributive bicategory of relations

References:

• Carboni & Walters, 1987, "Cartesian bicategories I", Remark 3.7 (mention in passing only)
• Patterson, 2017, "Knowledge representation in bicategories of relations", Section 9.2

FIXME: Should also inherit BicategoryOfRelations, but multiple inheritance is not yet supported.

Theory of a distributive category

A distributive category is a distributive monoidal category whose tensor product is the cartesian product, see DistributiveMonoidalCategory.

FIXME: Should also inherit CartesianCategory.

Theory of a distributive (symmetric) monoidal category

Reference: Jay, 1992, LFCS tech report LFCS-92-205, "Tail recursion through universal invariants", Section 3.2

FIXME: Should also inherit CocartesianCategory.

Theory of a distributive semiadditive category

This terminology is not standard but the concept occurs frequently. A distributive semiadditive category is a semiadditive category (or biproduct) category, written additively, with a tensor product that distributes over the biproduct.

FIXME: Should also inherit SemiadditiveCategory

Theory of hypergraph categories

Hypergraph categories are also known as "well-supported compact closed categories" and "spidered/dungeon categories", among other things.

FIXME: Should also inherit ClosedMonoidalCategory and DaggerCategory, but multiple inheritance is not yet supported.

Theory of hypergraph categories, in additive notation

Mathematically the same as HypergraphCategory but with different notation.

Theory of monoidal categories

To avoid associators and unitors, we assume the monoidal category is strict. By the coherence theorem there is no loss of generality, but we may add a theory for weak monoidal categories later.

Theory of monoidal categories, in additive notation

Mathematically the same as MonoidalCategory but with different notation.

Theory of monoidal categories with bidiagonals

The terminology is nonstandard (is there any standard terminology?) but is supposed to mean a monoidal category with coherent diagonals and codiagonals. Unlike in a biproduct category, the naturality axioms need not be satisfied.

Theory of monoidal categories with bidiagonals, in additive notation

Mathematically the same as MonoidalCategoryWithBidiagonals but written additively, instead of multiplicatively.

Theory of monoidal categories with codiagonals

A monoidal category with codiagonals is a symmetric monoidal category equipped with coherent collections of merging and creating morphisms (monoids). Unlike in a cocartesian category, the naturality axioms need not be satisfied.

For references, see MonoidalCategoryWithDiagonals.

Theory of monoidal categories with diagonals

A monoidal category with diagonals is a symmetric monoidal category equipped with coherent operations of copying and deleting, also known as a supply of commutative comonoids. Unlike in a cartesian category, the naturality axioms need not be satisfied.

References:

• Fong & Spivak, 2019, "Supplying bells and whistles in symmetric monoidal categories" (arxiv:1908.02633)
• Selinger, 2010, "A survey of graphical languages for monoidal categories", Section 6.6: "Cartesian center"
• Selinger, 1999, "Categorical structure of asynchrony"

Theory of preorders

Preorders encode the axioms of reflexivity and transitivity as term constructors.

Theory of a rig category, also known as a bimonoidal category

Rig categories are the most general in the hierarchy of distributive monoidal structures.

TODO: Do we also want the distributivty and absorption isomorphisms? Usually we ignore coherence isomorphisms such as associators and unitors.

FIXME: This theory should also inherit MonoidalCategory, but multiple inheritance is not supported.

The GAT that parameterizes Attributed C-sets

A schema is comprised of a category C, a discrete category D, and a profunctor Attr : C^op x D → Set. In GAT form, this is given by extending the theory of categories with two extra types, Data for objects of D, and Attr, for elements of the sets given by the profunctor.

Theory of semiadditive categories

Mathematically the same as BiproductCategory but written additively, instead of multiplicatively.

Theory of symmetric monoidal categories

The theory (but not the axioms) is the same as a braided monoidal category.

Theory of symmetric monoidal categories, in additive notation

Mathematically the same as SymmetricMonoidalCategory but with different notation.

Theory of a symmetric rig category

FIXME: Should also inherit SymmetricMonoidalCategory.

Theory of thin categories

Thin categories have at most one morphism between any two objects.

Theory of traced monoidal categories

Collect generators of object in monoidal category as a vector.

Number of "dimensions" of object in monoidal category.