# Standard library of theories

Through the module `Catlab.Theories`

, Catlab provides a standard library of generalized algebraic theories for categories, monoidal categories, and other categorical structures. The theories correspond, in most cases, to standard definitions in category theory and they are used throughout Catlab and the AlgebraicJulia ecosystem to structure programs and provide a common interface for applied category theory. The module also provides default syntax systems for many of the theories.

Categorical structures for which theories are provided include:

- categories
- monoidal and symmetric monoidal categories
- cartesian and cocartesian categories
- semiadditive categories/biproduct categories
- hypergraph categories
- bicategories of relations
- categories with two monoidal products, such as distributive monoidal categories

The contents of this module can be supplemented by the user, and it is even possible to use many parts of Catlab without using this module. The user is free to create new syntax systems for the theories defined here and also to define entirely new theories.

`Catlab.Theories`

— ModuleCatlab's standard library of generalized algebraic theories.

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

`Catlab.Theories.AbelianBicategoryRelations`

— TypeTheory 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"

`Catlab.Theories.AdditiveCategory`

— TypeTheory of *additive categories*

An additive category is a biproduct category enriched in abelian groups. Thus, it is a semiadditive category where the hom-monoids have negatives.

`Catlab.Theories.AlgebraicLattice`

— TypeTheory of *lattices* as algebraic structures

This is one of two standard axiomatizations of a lattice, the other being `Lattice`

. Because the partial order is not present, this theory is merely an algebraic theory (no dependent types).

The partial order is recovered as $A ≤ B$ iff $A ∧ B = A$ iff $A ∨ B = B$. This definition could be reintroduced into a generalized algebraic theory using an equality type `Eq(lhs::El, rhs::El)::TYPE`

combined with term constructors ``meet_leq(eq::Eq(A∧B, A))::(A ≤ B)`

and `join_leq(eq::Eq(A∨B, B))::(A ≤ B)`

. We do not employ that trick here because at that point it is more convenient to just start with the poset structure, as in `Lattice`

.

`Catlab.Theories.BicategoryRelations`

— TypeTheory 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

`Catlab.Theories.BiproductCategory`

— TypeTheory of *biproduct categories*

Mathematically the same as `SemiadditiveCategory`

but written multiplicatively, instead of additively.

`Catlab.Theories.CartesianCategory`

— TypeTheory of *cartesian (monoidal) categories*

For the traditional axiomatization of products, see `CategoryWithProducts`

.

`Catlab.Theories.CartesianClosedCategory`

— TypeTheory 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.

`Catlab.Theories.Category`

— TypeTheory 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).

`Catlab.Theories.Category2`

— TypeTheory of (strict) *2-categories*

`Catlab.Theories.CategoryWithCoproducts`

— TypeTheory 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`

.

`Catlab.Theories.CategoryWithProducts`

— TypeTheory 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`

.

`Catlab.Theories.ClosedMonoidalCategory`

— TypeTheory of (symmetric) *closed monoidal categories*

`Catlab.Theories.CocartesianCategory`

— TypeTheory of *cocartesian (monoidal) categories*

For the traditional axiomatization of coproducts, see `CategoryWithCoproducts`

.

`Catlab.Theories.CocompleteCategory`

— TypeTheory 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`

.

`Catlab.Theories.CompactClosedCategory`

— TypeTheory of *compact closed categories*

`Catlab.Theories.CompleteCategory`

— TypeTheory 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".

`Catlab.Theories.Copresheaf`

— TypeTheory of *copresheaves*.

Axiomatized as a covariant category action.

`Catlab.Theories.DaggerCategory`

— TypeTheory of *dagger categories*

`Catlab.Theories.DaggerCompactCategory`

— TypeTheory 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.

`Catlab.Theories.DaggerSymmetricMonoidalCategory`

— TypeTheory 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.

`Catlab.Theories.DisplayedCategory`

— TypeTheory of a *displayed category*.

More precisely, this is the theory of a base category $C$ (`Ob`

,`Hom`

) and a displayed category (`El`

,`Act`

) over $C$. Displayed categories axiomatize lax functors $C → **Span**$ or equivalently objects in $**Cat**/C$ in a pleasant, generalized algebraic style.

Reference: Ahrens & Lumsdaine 2019, "Displayed categories", Definition 3.1.

`Catlab.Theories.DistributiveBicategoryRelations`

— TypeTheory 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.

`Catlab.Theories.DistributiveCategory`

— TypeTheory 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`

.

`Catlab.Theories.DistributiveMonoidalCategory`

— TypeTheory 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`

.

`Catlab.Theories.DistributiveSemiadditiveCategory`

— TypeTheory 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`

`Catlab.Theories.DoubleCategory`

— TypeTheory of (strict) *double categories*

`Catlab.Theories.HypergraphCategory`

— TypeTheory 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.

`Catlab.Theories.HypergraphCategoryAdditive`

— TypeTheory of *hypergraph categories*, in additive notation

Mathematically the same as `HypergraphCategory`

but with different notation.

`Catlab.Theories.Lattice`

— TypeTheory of *lattices* as posets

A (bounded) lattice is a poset with all finite meets and joins. Viewed as a thin category, this means that the category has all finite products and coproducts, hence the names for the inequality constructors in the theory. Compare with `CartesianCategory`

and `CocartesianCategory`

.

This is one of two standard axiomatizations of a lattice, the other being `AlgebraicLattice`

.

`Catlab.Theories.MonoidalCategory`

— TypeTheory 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.

`Catlab.Theories.MonoidalCategoryAdditive`

— TypeTheory of *monoidal categories*, in additive notation

Mathematically the same as `MonoidalCategory`

but with different notation.

`Catlab.Theories.MonoidalCategoryWithBidiagonals`

— TypeTheory 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.

`Catlab.Theories.MonoidalCategoryWithBidiagonalsAdditive`

— TypeTheory of *monoidal categories with bidiagonals*, in additive notation

Mathematically the same as `MonoidalCategoryWithBidiagonals`

but written additively, instead of multiplicatively.

`Catlab.Theories.MonoidalCategoryWithCodiagonals`

— TypeTheory 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`

.

`Catlab.Theories.MonoidalCategoryWithDiagonals`

— TypeTheory 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"

`Catlab.Theories.MonoidalDoubleCategory`

— TypeTheory of *monoidal double categories*

To avoid associators and unitors, we assume the monoidal double category is *strict* in both the horizontal and vertical directions. Apart from assuming strictness, this theory follows the definition of a monoidal double category in (Shulman, 2010, Constructing symmetric monoidal bicategories) and other recent papers, starting from an internal category $(S,T: D₁ ⇉ D₀, U: D₀ → D₁, *: D₁ ×_{D₀} D₁ → D₁)$ in **Cat** where

- the objects of $D₀$ are objects
- the morphisms of $D₀$ are vertical 1-cells
- the objects of $D₁$ are horizontal 1-cells
- the morphisms of $D₁$ are 2-cells.

The top and bottom of a 2-cell are given by domain and codomain in $D₁$ and the left and right are given by the functors $S,T$. In a monoidal double category, $D₀$ and $D₁$ are each required to be monoidal categories, subject to further axioms such as $S$ and $T$ being strict monoidal functors.

Despite the apparent asymmetry in this setup, the definition of a monoidal double category unpacks to be nearly symmetric with respect to horizontal and vertical, except that the monoidal unit $I$ of $D₀$ induces the monoidal unit of $D₁$ as $U(I)$, which I think has no analogue in the vertical direction.

`Catlab.Theories.Poset`

— TypeTheory of *partial orders* (posets)

`Catlab.Theories.Preorder`

— TypeTheory of *preorders*

The generalized algebraic theory of preorders encodes inequalities $A≤B$ as dependent types `$Leq(A,B)$ and the axioms of reflexivity and transitivity as term constructors.

`Catlab.Theories.Presheaf`

— TypeTheory of *presheaves*.

Axiomatized as a contravariant category action.

`Catlab.Theories.RigCategory`

— TypeTheory 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.

`Catlab.Theories.Schema`

— TypeThe 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, AttrType for objects of D, and Attr, for elements of the sets given by the profunctor.

`Catlab.Theories.SemiadditiveCategory`

— TypeTheory of *semiadditive categories*

Mathematically the same as `BiproductCategory`

but written additively, instead of multiplicatively.

`Catlab.Theories.SymmetricMonoidalCategory`

— TypeTheory of (strict) *symmetric monoidal categories*

`Catlab.Theories.SymmetricMonoidalCategoryAdditive`

— TypeTheory of *symmetric monoidal categories*, in additive notation

Mathematically the same as `SymmetricMonoidalCategory`

but with different notation.

`Catlab.Theories.SymmetricMonoidalCopresheaf`

— TypeTheory of a *symmetric monoidal copresheaf*

The name is not standard but refers to a lax symmetric monoidal functor into **Set**. This can be interpreted as an action of a symmetric monoidal category, just as a copresheaf (set-valued functor) is an action of a category. The theory is simpler than that of a general lax monoidal functor because (1) the domain is a strict monoidal category and (2) the codomain is fixed to the cartesian monoidal category **Set**.

FIXME: This theory should also extend `Copresheaf`

but multiple inheritance is not yet supported.

`Catlab.Theories.SymmetricMonoidalDoubleCategory`

— TypeTheory of (strict) *symmetric monoidal double categories*

Unlike classical double categories, symmetric monoidal double categories do not treat the vertical and horizontal directions on an equal footing, even in the strict case. See `MonoidalDoubleCategory`

for details and references.

`Catlab.Theories.SymmetricRigCategory`

— TypeTheory of a *symmetric rig category*

FIXME: Should also inherit `SymmetricMonoidalCategory`

.

`Catlab.Theories.ThinCategory`

— TypeTheory of *thin categories*

Thin categories have at most one morphism between any two objects and are isomorphic to preorders.

`Catlab.Theories.ThinSymmetricMonoidalCategory`

— TypeTheory of *thin symmetric monoidal category*

Thin SMCs are isomorphic to commutative monoidal prosets.

`Catlab.Theories.TracedMonoidalCategory`

— TypeTheory of *traced monoidal categories*

`Base.collect`

— MethodCollect generators of object in monoidal category as a vector.

`Base.ndims`

— MethodNumber of "dimensions" of object in monoidal category.