Catlab.Doctrines API

# Catlab.Doctrines API

Doctrine of abelian bicategory of relations

Unlike Carboni & Walters, we use additive notation and nomenclature.

References:

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

Doctrine of bicategory of relations

TODO: The 2-morphisms are missing. I haven't decided how to handle them yet.

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
source

Doctrine of bicategory category

Also known as a semiadditive category.

FIXME: This signature should extend MonoidalCategoryWithBidiagonals, CartesianCategory, and CocartesianCategory, but we don't support multiple inheritance.

source

Doctrine of cartesian category

Actually, this is a cartesian symmetric monoidal category but we omit these qualifiers for brevity.

source

Doctrine of cartesian closed category (aka, CCC)

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

source

Doctrine of category (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).

source

Doctrine of (strict) 2-category

source

Doctrine of cocartesian category

Actually, this is a cocartesian symmetric monoidal category but we omit these qualifiers for brevity.

source

Doctrine of compact closed category

source

Doctrine of dagger category

source

Doctrine of dagger compact category

FIXME: This signature should extend both DaggerCategory and CompactClosedCategory, but we don't support multiple inheritance yet.

source

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. Of course, this convention could be reversed.

source

Syntax for a free cartesian closed category.

See also FreeCartesianCategory.

source

Syntax for a 2-category.

Checks domains of morphisms but not 2-morphisms.

source

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. Of course, this convention could be reversed.

source

Doctrine of monoidal category

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 signature for weak monoidal categories later.

source

Doctrine of monoidal category with bidiagonals

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

FIXME: This signature should extend both MonoidalCategoryWithDiagonals and MonoidalCategoryWithCodiagonals, but we don't support multiple inheritance.

source

Doctrine of monoidal category 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.

source

Doctrine of monoidal category with diagonals

A monoidal category with diagonals is a symmetric monoidal category equipped with coherent collections of copying and deleting morphisms (comonoids). Unlike in a cartesian category, the naturality axioms need not be satisfied.

References:

• Selinger, 2010, "A survey of graphical languages for monoidal categories", Section 6.6: "Cartesian center"
• Selinger, 1999, "Categorical structure of asynchrony"
source

Doctrine of symmetric monoidal category

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

source

Collect generators of object in monoidal category as a vector.

source

Number of "dimensions" of object in monoidal category.

source

Morphism in a category

source

Object in a category

source

Morphism in a category

source

Object in a category

source

Morphism in a category

source

Object in a category

source

Morphism in a category

source

Object in a category

source

Morphism in a category

source

Object in a category

source

Morphism in a category

source

Object in a category

source

Morphism in a category

source

2-morphism in a 2-category

source

Object in a category

source

Morphism in a category

source

Object in a category

source

Morphism in a category

source

Object in a category

source

Morphism in a category

source

Object in a category

source

Morphism in a category

source

Object in a category

source

Morphism in a category

source

Object in a category

source

Morphism in a category

source

Object in a category

source

Morphism in a category

source

Object in a category

source

Morphism in a category

source

Object in a category

source

Morphism in a category

source

Object in a category

source

Morphism in a category

source

Object in a category

source

Morphism in a category

source

2-morphism in a 2-category

source

Object in a category

source

Morphism in a category

source

Object in a category

source

Morphism in a category

source

Object in a category

source

Morphism in a category

source

Object in a category

source

Morphism in a category

source

Object in a category

source

Morphism in a category

source

Object in a category

source

Morphism in a category

source

Object in a category

source

Morphism in a category

source

Object in a category

source

Morphism in a category

source

Object in a category

source

Morphism in a category

source

Object in a category

source

Morphism in a category

source

Object in a category

source