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.CategoryExpr
— TypeBase type for GAT expressions in categories or other categorical structures.
All symbolic expression types exported by Catlab.Theories
are subtypes of this abstract type.
Catlab.Theories.HomExpr
— TypeBase type for morphism expressions in categorical structures.
Catlab.Theories.ObExpr
— TypeBase type for object expressions in categorical structures.
Catlab.Theories.ThAbelianBicategoryRelations
— TypeTheory of abelian bicategories of relations
Unlike ThBicategoryRelations
, this theory uses additive notation.
References:
- Carboni & Walters, 1987, "Cartesian bicategories I", Sec. 5
- Baez & Erbele, 2015, "Categories in control"
Catlab.Theories.ThAdditiveCategory
— 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.ThAlgebraicLattice
— TypeTheory of lattices as algebraic structures
This is one of two standard axiomatizations of a lattice, the other being ThLattice
. 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 ThLattice
.
Catlab.Theories.ThBicategoryRelations
— 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.ThBiproductCategory
— TypeTheory of biproduct categories
Mathematically the same as ThSemiadditiveCategory
but written multiplicatively, instead of additively.
Catlab.Theories.ThCartesianCategory
— TypeTheory of cartesian (monoidal) categories
For the traditional axiomatization of products, see ThCategoryWithProducts
.
Catlab.Theories.ThCartesianClosedCategory
— 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 ThClosedMonoidalCategory
, but multiple inheritance is not yet supported.
Catlab.Theories.ThCartesianDoubleCategory
— TypeTheory of a cartesian double category
Loosely speaking, a cartesian double category is a double category $D$ such that the underlying catgories $D₀$ and $D₁$ are both cartesian categories, in a compatible way.
Reference: Aleiferi 2018, PhD thesis.
Catlab.Theories.ThCategory
— TypeTheory of categories
Note: Throughout Catlab, we compose morphisms in diagrammatic order (from left to right), i.e., if $f:A→B$ and $g:B→C$ then the composite morphism $f⋅g:A→C$ is compose(f,g)
. Under this convention, functions 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$ is compose(f,g)
. This usage is too entrenched to overturn. However, we use the symbol $⋅$ (\cdot
) for composition in diagrammatic order.
Catlab.Theories.ThCategory2
— TypeTheory of 2-categories
Catlab.Theories.ThCategoryWithCoproducts
— 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 ThCategoryWithProducts
.
For a monoidal category axiomatization of finite coproducts, see ThCocartesianCategory
.
Catlab.Theories.ThCategoryWithProducts
— 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 of finite products, see ThCartesianCategory
.
Catlab.Theories.ThClosedMonoidalCategory
— TypeTheory of (symmetric) closed monoidal categories
Catlab.Theories.ThCocartesianCategory
— TypeTheory of cocartesian (monoidal) categories
For the traditional axiomatization of coproducts, see ThCategoryWithCoproducts
.
Catlab.Theories.ThCocompleteCategory
— 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 ThCompleteCategory
.
Catlab.Theories.ThCompactClosedCategory
— TypeTheory of compact closed categories
Catlab.Theories.ThCompleteCategory
— 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), who in turn attribute them to "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.ThCopresheaf
— TypeTheory of copresheaves.
Axiomatized as a covariant category action.
Catlab.Theories.ThDaggerCategory
— TypeTheory of dagger categories
Catlab.Theories.ThDaggerCompactCategory
— 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 ThDaggerCategory
, but multiple inheritance is not yet supported.
Catlab.Theories.ThDaggerSymmetricMonoidalCategory
— TypeTheory of dagger symmetric monoidal categories
Also known as a symmetric monoidal dagger category.
FIXME: This theory should also extend ThDaggerCategory
, but multiple inheritance is not yet supported.
Catlab.Theories.ThDisplayedCategory
— TypeTheory of a displayed category.
More precisely, this is the theory of a category $C$ (Ob
,Hom
) together with a displayed category over $C$ (Fib
,FibHom
). Displayed categories axiomatize lax functors $C → **Span**$, or equivalently objects of a slice category $**Cat**/C$, in a generalized algebraic style.
Reference: Ahrens & Lumsdaine 2019, "Displayed categories", Definition 3.1.
Catlab.Theories.ThDistributiveBicategoryRelations
— 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 ThBicategoryOfRelations
, but multiple inheritance is not yet supported.
Catlab.Theories.ThDistributiveCategory
— TypeTheory of a distributive category
A distributive category is a distributive monoidal category whose tensor product is the cartesian product, see ThDistributiveMonoidalCategory
.
FIXME: Should also inherit ThCartesianCategory
.
Catlab.Theories.ThDistributiveMonoidalCategory
— 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 ThCocartesianCategory
.
Catlab.Theories.ThDistributiveSemiadditiveCategory
— 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 ThSemiadditiveCategory
Catlab.Theories.ThDoubleCategory
— TypeTheory of double categories
A strict double category $D$ is an internal category
$(S,T: D₁ ⇉ D₀, U: D₀ → D₁, *: D₁ ×_{D₀} D₁ → D₁)$
in Cat where
- objects of $D₀$ are objects of $D$
- morphisms of $D₀$ are arrows (vertical morphisms) of $D$
- objects of $D₁$ are proarrows (horizontal morphisms) of $D$
- morphisms of $D₁$ are cells of $D$.
The domain and codomain (top and bottom) of a cell are given by the domain and codomain in $D₁$ and the source and target (left and right) are given by the functors $S,T$.
Catlab.Theories.ThDoubleCategoryWithTabulators
— TypeTheory of a double category with tabulators
A tabulator of a proarrow is a double-categorical limit. It is a certain cell with identity domain to the given proarrow that is universal among all cells of that form. A double category "has tabulators" if the external identity functor has a right adjoint. The values of this right adjoint are the apex objects of its tabulators. The counit of the adjunction provides the universal cells. Tabulators figure in the double-categorical limit construction theorem of Grandis-Pare 1999. In the case where the double category is actually a 2-category, tabulators specialize to cotensors, a more familiar 2-categorical limit.
Catlab.Theories.ThEquipment
— TypeTheory of a proarrow equipment, or equipment for short
Equipments have also been called "framed bicategories," "fibrant double categories," and "gregarious double categories" (?!).
References:
- Shulman, 2008: Framed bicategories and monoidal fibrations
- Cruttwell & Shulman, 2010: A unified framework for generalized multicategories
Catlab.Theories.ThGroupoid
— TypeTheory of groupoids.
Catlab.Theories.ThHypergraphCategory
— 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 ThClosedMonoidalCategory
and ThDaggerCategory
, but multiple inheritance is not yet supported.
Catlab.Theories.ThHypergraphCategoryAdditive
— TypeTheory of hypergraph categories, in additive notation
Mathematically the same as HypergraphCategory
but with different notation.
Catlab.Theories.ThIndexedCategory
— TypeTheory of a (covariantly) indexed category.
An indexed category is a Cat-valued pseudofunctor. For simplicitly, we assume that the functor is strict.
Just as a copresheaf, or Set-valued functor, can be seen as a category action of a family of sets, an indexed category can be seen as a category action on a family of categories. This picture guides our axiomatization of an indexed category as a generalized algebraic theory.
Catlab.Theories.ThIndexedMonoidalCategory
— TypeTheory of a (covariantly) indexed monoidal category.
An indexed monoidal category is a pseudofunctor into MonCat, the 2-category of monoidal categories, lax monoidal functor, and monoidal natural transformations. As usual, we take both the pseudofunctor and the monoidal categories to be strict. However, unlike the most common definition of an indexed monoidal category (see nLab), we allow the transition functors between monoidal categories to be lax monoidal. This follows the usage in (Hofstra & De Marchi 2006).
References:
- Hofstra & De Marchi, 2006: Descent for monads
- Moeller & Vasilakopoulou, 2020: Monoidal Grothendieck construction, Remark 3.18 [this paper is about a different notion!]
Catlab.Theories.ThLattice
— 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 ThCartesianCategory
and ThCocartesianCategory
.
This is one of two standard axiomatizations of a lattice, the other being ThAlgebraicLattice
.
Catlab.Theories.ThMCategory
— TypeTheory of an ℳ-category.
The term "ℳ-category", used on the nLab is not very common, but the concept itself shows up commonly. An ℳ-category is a category with a distinguished wide subcategory, whose morphisms are suggestively called tight; for contrast, a generic morphism is called loose. Equivalently, an ℳ-category is a category enriched in the category ℳ of injections, the full subcategory of the arrow category of Set spanned by injections.
In the following GAT, tightness is axiomatized as a property of morphisms: a dependent family of sets over the hom-sets, each having at most one inhabitant.
Catlab.Theories.ThMonoidalCategory
— TypeTheory of monoidal categories
To avoid associators and unitors, we assume that the monoidal category is strict. By the coherence theorem this involves no loss of generality, but we might add a theory for weak monoidal categories later.
Catlab.Theories.ThMonoidalCategoryAdditive
— TypeTheory of monoidal categories, in additive notation
Mathematically the same as ThMonoidalCategory
but with different notation.
Catlab.Theories.ThMonoidalCategoryWithBidiagonals
— 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.ThMonoidalCategoryWithBidiagonalsAdditive
— TypeTheory of monoidal categories with bidiagonals, in additive notation
Mathematically the same as MonoidalCategoryWithBidiagonals
but written additively, instead of multiplicatively.
Catlab.Theories.ThMonoidalCategoryWithCodiagonals
— 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 ThMonoidalCategoryWithDiagonals
.
Catlab.Theories.ThMonoidalCategoryWithDiagonals
— 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.ThMonoidalDoubleCategory
— TypeTheory of monoidal double categories
To avoid associators and unitors, we assume that the monoidal double category is fully strict: both the double category and its monoidal product are strict. Apart from assuming strictness, this theory agrees with the definition of a monoidal double category in (Shulman 2010) and other recent works.
In a monoidal double category $(D,⊗,I)$, the underlying categories $D₀$ and $D₁$ are each monoidal categories, $(D₀,⊗₀,I₀)$ and $(D₁,⊗₁,I₁)$, subject to further axioms such as the source and target functors $S, T: D₁ → D₀$ 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 arrows and proarrows, except that the monoidal unit $I₀$ of $D₀$ induces the monoidal unit of $D₁$ as $I₁ = U(I₀)$.
References:
- Shulman, 2010: Constructing symmetric monoidal bicategories
FIXME: Should also inherit ThMonoidalCategory{Ob,Hom}
but multiple inheritance is not supported.
Catlab.Theories.ThPoset
— TypeTheory of partial orders (posets)
Catlab.Theories.ThPreorder
— 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.ThPresheaf
— TypeTheory of presheaves.
Axiomatized as a contravariant category action.
Catlab.Theories.ThRigCategory
— TypeTheory of a rig category, also known as a bimonoidal category
Rig categories are the most general in the hierarchy of distributive monoidal structures.
Question: 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 ThMonoidalCategory
, but multiple inheritance is not supported.
Catlab.Theories.ThSchema
— 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.ThSemiadditiveCategory
— TypeTheory of semiadditive categories
Mathematically the same as BiproductCategory
but written additively, instead of multiplicatively.
Catlab.Theories.ThSymmetricMonoidalCategory
— TypeTheory of (strict) symmetric monoidal categories
Catlab.Theories.ThSymmetricMonoidalCategoryAdditive
— TypeTheory of symmetric monoidal categories, in additive notation
Mathematically the same as ThSymmetricMonoidalCategory
but with different notation.
Catlab.Theories.ThSymmetricMonoidalCopresheaf
— 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 ThCopresheaf
but multiple inheritance is not yet supported.
Catlab.Theories.ThSymmetricMonoidalDoubleCategory
— TypeTheory of symmetric monoidal double categories
Unlike the classical notion of strict double categories, symmetric monoidal double categories do not treat the two directions on an equal footing, even when everything (except the braiding) is strict. See MonoidalDoubleCategory
for references.
FIXME: Should also inherit ThSymmetricMonoidalCategory{Ob,Hom}
but multiple inheritance is not supported.
Catlab.Theories.ThSymmetricRigCategory
— TypeTheory of a symmetric rig category
FIXME: Should also inherit ThSymmetricMonoidalCategory
.
Catlab.Theories.ThThinCategory
— TypeTheory of thin categories
Thin categories have at most one morphism between any two objects and are isomorphic to preorders.
Catlab.Theories.ThThinSymmetricMonoidalCategory
— TypeTheory of thin symmetric monoidal category
Thin SMCs are isomorphic to commutative monoidal prosets.
Catlab.Theories.ThTracedMonoidalCategory
— 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.