Categorical algebra

Category of (possibly infinite) sets and functions.

This module defines generic types for the category of sets (SetOb, SetFunction), as well as a few basic concrete types, such as a wrapper type to view Julia types as sets (TypeSet). Extensive support for finite sets is provided by another module, FinSets.

Function in Set taking a constant value.

Set defined by a predicate (boolean-valued function) on a Julia data type.

Abstract type for morphism in the category Set.

Every instance of SetFunction{<:SetOb{T},<:SetOb{T′}} is callable with elements of type T, returning an element of type T′.

Note: This type would be better called simply Function but that name is already taken by the base Julia type.

Abstract type for object in the category Set.

The type parameter T is the element type of the set.

Note: This type is more abstract than the built-in Julia types AbstractSet and Set, which are intended for data structures for finite sets. Those are encompassed by the subtype FinSet.

A Julia data type regarded as a set.

Forgetful functor Ob: Cat → Set.

Sends a category to its set of objects and a functor to its object map.

The category of finite sets and functions, and its skeleton.

Function out of a finite set.

This class of functions is convenient because it is exactly the class that can be represented explicitly by a vector of values from the codomain.

Function between finite sets.

The function can be defined implicitly by an arbitrary Julia function, in which case it is evaluated lazily, or explictly by a vector of integers. In the vector representation, the function (1↦1, 2↦3, 3↦2, 4↦3), for example, is represented by the vector [1,3,2,3].

This type is mildly generalized by FinDomFunction.

Finite set.

A finite set has abstract type FinSet{S,T}. The second type parameter T is the element type of the set and the first parameter S is the collection type, which can be a subtype of AbstractSet or another Julia collection type. In addition, the skeleton of the category FinSet is the important special case S = Int. The set ${1,…,n}$ is represented by the object FinSet(n) of type FinSet{Int,Int}.

Hash join algorithm.

Algorithm for limit of cospan or multicospan with feet being finite sets.

In the context of relational databases, such limits are called joins. The trivial join algorithm is NestedLoopJoin, which is algorithmically equivalent to the generic algorithm ComposeProductEqualizer. The algorithms HashJoin and SortMergeJoin are usually much faster. If you are unsure what algorithm to pick, use SmartJoin.

Nested-loop join algorithm.

This is the naive algorithm for computing joins.

Meta-algorithm for joins that attempts to pick an appropriate algorithm.

Sort-merge join algorithm.

Subset of a finite set.

Algorithm to compute subobject operations using elementwise boolean logic.

Limit of finite sets viewed as a table.

Any limit of finite sets can be canonically viewed as a table (TabularSet) whose columns are the legs of the limit cone and whose rows correspond to elements of the limit object. To construct this table from an already computed limit, call TabularLimit(::AbstractLimit; ...). The column names of the table are given by the optional argument names.

In this tabular form, applying the universal property of the limit is trivial since it is just tupling. Thus, this representation can be useful when the original limit algorithm does not support efficient application of the universal property. On the other hand, this representation has the disadvantage of generally making the element type of the limit set more complicated.

Finite set whose elements are rows of a table.

The underlying table should be compliant with Tables.jl. For the sake of uniformity, the rows are provided as named tuples, which assumes that the table is not "extremely wide". This should not be a major limitation in practice but see the Tables.jl documentation for further discussion.

Whether the given function is indexed, i.e., supports efficient preimages.

The preimage (inverse image) of the value y in the codomain.

The category of finite sets and relations, and its skeleton.

The rig of booleans.

This struct is needed because in base Julia, the product of booleans is another boolean, but the sum of booleans is coerced to an integer: true + true == 2.

Object in the category of finite sets and relations.

See also: FinSet.

Binary relation between finite sets.

A morphism in the category of finite sets and relations. The relation can be represented implicitly by an arbitrary Julia function mapping pairs of elements to booleans or explicitly by a matrix (dense or sparse) taking values in the rig of booleans (BoolRig).

Relation in FinRel defined by a callable Julia object.

Relation in FinRel represented by a boolean matrix.

Boolean matrices are also known as logical matrices or relation matrices.

Free diagrams in a category.

A free diagram in a category is a diagram whose shape is a free category. Examples include the empty diagram, pairs of objects, discrete diagrams, parallel pairs, composable pairs, and spans and cospans. Limits and colimits are most commonly taken over free diagrams.

A free diagram with a bipartite structure.

Such diagrams include most of the fixed shapes, such as spans, cospans, and parallel morphisms. They are also the generic shape of diagrams for limits and colimits arising from undirected wiring diagrams. For limits, the boxes correspond to vertices in $V₁$ and the junctions to vertices in $V₂$. Colimits are dual.

Convert a free diagram to a bipartite free diagram.

Reduce a free diagram to a free bipartite diagram with the same limit (the default, colimit=false) or the same colimit (colimit=true). The reduction is essentially the same in both cases, except for the choice of where to put isolated vertices, where we follow the conventions described at cone_objects and cocone_objects. The resulting object is a bipartite free diagram equipped with maps from the vertices of the bipartite diagram to the vertices of the original diagram.

Composable morphisms in a category.

Composable morphisms are a sequence of morphisms in a category that form a path in the underlying graph of the category.

For the common special case of two morphisms, see ComposablePair.

Pair of composable morphisms in a category.

Composable pairs are a common special case of ComposableMorphisms.

Cospan of morphisms in a category.

A common special case of Multicospan. See also Span.

Discrete diagram: a diagram with no non-identity morphisms.

Abstract type for free diagram of fixed shape.

Multicospan of morphisms in a category.

A multicospan is like a Cospan except that it may have a number of legs different than two. A limit of this shape is a pullback.

Multispan of morphisms in a category.

A multispan is like a Span except that it may have a number of legs different than two. A colimit of this shape is a pushout.

Parallel morphims in a category.

Parallel morphisms are just morphisms with the same domain and codomain. A (co)limit of this shape is a (co)equalizer.

For the common special case of two morphisms, see ParallelPair.

Pair of parallel morphisms in a category.

A common special case of ParallelMorphisms.

Span of morphims in a category.

A common special case of Multispan. See also Cospan.

Apex of multispan or multicospan.

The apex of a multi(co)span is the object that is the (co)domain of all the legs.

Bundle together legs of a multi(co)span.

For example, calling bundle_legs(span, SVector((1,2),(3,4))) on a multispan with four legs gives a span whose left leg bundles legs 1 and 2 and whose right leg bundles legs 3 and 4. Note that in addition to bundling, this function can also permute legs and discard them.

The bundling is performed using the universal property of (co)products, which assumes that these (co)limits exist.

Objects in diagram that will have explicit legs in colimit cocone.

See also: cone_objects.

Objects in diagram that will have explicit legs in limit cone.

In category theory, it is common practice to elide legs of limit cones that can be computed from other legs, especially for diagrams of certain fixed shapes. For example, when it taking a pullback (the limit of a cospan), the limit object is often treated as having two projections, rather than three. This function encodes such conventions by listing the objects in the diagram that will have corresponding legs in the limit object created by Catlab.

See also: cocone_objects.

Given a diagram in a category $C$, return Julia type of objects and morphisms in $C$ as a tuple type of form $Tuple{Ob,Hom}$.

Feet of multispan or multicospan.

The feet of a multispan are the codomains of the legs.

Left leg of span or cospan.

Legs of multispan or multicospan.

The legs are the morphisms comprising the multi(co)span.

Right leg of span or cospan.

Limits and colimits in a category.

Abstract type for colimit in a category.

The standard concrete subtype is Colimit, although for computational reasons certain categories may use different subtypes to include extra data.

Abstract type for limit in a category.

The standard concrete subtype is Limit, although for computational reasons certain categories may use different subtypes to include extra data.

Colimit in a category.

Algorithm for computing colimits.

Compute pushout by composing a coproduct with a coequalizer.

See also: ComposeProductEqualizer.

Compute pullback by composing a product with an equalizer.

See also: ComposeCoproductCoequalizer.

Limit in a category.

Algorithm for computing limits.

Meta-algorithm that reduces general colimits to common special cases.

Dual to SpecializeLimit.

Meta-algorithm that reduces general limits to common special cases.

Reduces limits of free diagrams that happen to be discrete to products. If this fails, fall back to the given algorithm (if any).

TODO: Reduce free diagrams that are (multi)cospans to (wide) pullbacks.

Compute a colimit by reducing the diagram to a free bipartite diagram.

Compute a limit by reducing the diagram to a free bipartite diagram.

https://en.wikipedia.org/wiki/Coimage

Colimit of a diagram.

To define colimits in a category with objects Ob, override the method colimit(::FreeDiagram{Ob}) for general colimits or colimit(::D) with suitable type D <: FixedShapeFreeDiagram{Ob} for colimits of specific shape, such as coproducts or coequalizers.

See also: limit

The image and coimage are isomorphic. We get this isomorphism using univeral properties.

  CoIm′ ╌╌> I ↠ CoIm
    ┆ ⌟     |
    v       v
    I   ⟶  R ↩ Im
    |       ┆
    v    ⌜  v
    R ╌╌> Im′

https://en.wikipedia.org/wiki/Image(categorytheory)#Second_definition

Limit of a diagram.

To define limits in a category with objects Ob, override the method limit(::FreeDiagram{Ob}) for general limits or limit(::D) with suitable type D <: FixedShapeFreeDiagram{Ob} for limits of specific shape, such as products or equalizers.

See also: colimit

Pullback of a pair of morphisms with common codomain.

To implement for a type T, define the method limit(::Cospan{T}) and/or limit(::Multicospan{T}) or, if you have already implemented products and equalizers, rely on the default implementation.

Pushout of a pair of morphisms with common domain.

To implement for a type T, define the method colimit(::Span{T}) and/or colimit(::Multispan{T}) or, if you have already implemented coproducts and coequalizers, rely on the default implementation.

Coequalizer of morphisms with common domain and codomain.

To implement for a type T, define the method colimit(::ParallelPair{T}) or colimit(::ParallelMorphisms{T}).

Copairing of morphisms: universal property of coproducts/pushouts.

To implement for coproducts of type T, define the method universal(::BinaryCoproduct{T}, ::Cospan{T}) and/or universal(::Coproduct{T}, ::Multicospan{T}) and similarly for pushouts.

Coproduct of objects.

To implement for a type T, define the method colimit(::ObjectPair{T}) and/or colimit(::DiscreteDiagram{T}).

Unique morphism out of an initial object.

To implement for a type T, define the method universal(::Initial{T}, ::SMulticospan{0,T}).

Unique morphism into a terminal object.

To implement for a type T, define the method universal(::Terminal{T}, ::SMultispan{0,T}).

Equalizer of morphisms with common domain and codomain.

To implement for a type T, define the method limit(::ParallelPair{T}) and/or limit(::ParallelMorphisms{T}).

Factor morphism through (co)equalizer, via the universal property.

To implement for equalizers of type T, define the method universal(::Equalizer{T}, ::SMultispan{1,T}). For coequalizers of type T, define the method universal(::Coequalizer{T}, ::SMulticospan{1,T}).

Initial object.

To implement for a type T, define the method colimit(::EmptyDiagram{T}).

Pairing of morphisms: universal property of products/pullbacks.

To implement for products of type T, define the method universal(::BinaryProduct{T}, ::Span{T}) and/or universal(::Product{T}, ::Multispan{T}) and similarly for pullbacks.

Product of objects.

To implement for a type T, define the method limit(::ObjectPair{T}) and/or limit(::DiscreteDiagram{T}).

Terminal object.

To implement for a type T, define the method limit(::EmptyDiagram{T}).

Universal property of (co)limits.

Compute the morphism whose existence and uniqueness is guaranteed by the universal property of (co)limits.

See also: limit, colimit.

Define cartesian monoidal structure using limits.

Implements an instance of ThCartesianCategory assuming that finite products have been implemented following the limits interface.

Define cocartesian monoidal structure using colimits.

Implements an instance of ThCocartesianCategory assuming that finite coproducts have been implemented following the colimits interface.

2-category of categories, functors, and natural transformations.

Categories in mathematics appear in the large, often as categories of sets with extra structure, and in the small, as algebraic structures that generalize groups, monoids, preorders, and graphs. This division manifests in Catlab as well. Large categories (in spirit, if not in the technical sense) occur throughout Catlab as @instances of the theory of categories. For computational reasons, small categories are usually presented by generators and relations.

This module provides a minimal interface to accomodate both situations. Category instances are supported through the wrapper type TypeCat. Finitely presented categories are provided by another module, FinCats.

Alias for Category.

Size of a category, used for dispatch and subtyping purposes.

A Category type having a particular CatSize means that categories of that type are at most that large.

Abstract base type for a category.

The objects and morphisms in the category have Julia types Ob and Hom, respectively. Note that these types do not necessarily form an @instance of the theory of categories, as they may not meaningfully form a category outside the context of this object. For example, a finite category regarded as a reflexive graph with a composition operation might have type Cat{Int,Int}, where the objects and morphisms are numerical identifiers for vertices and edges in the graph.

The basic operations available in any category are: dom, codom, id, compose.

Composite of functors.

Abstract base type for a functor between categories.

A functor has a domain and a codomain (dom and codom), which are categories, and object and morphism maps, which can be evaluated using ob_map and hom_map. The functor object can also be called directly when the objects and morphisms have distinct Julia types. This is sometimes but not always the case (see Category), so when writing generic code one should prefer the ob_map and hom_map functions.

Functor defined by two Julia callables, an object map and a morphism map.

Identity functor on a category.

Size of a large category, such as Set.

To the extent that they form a category, we regard Julia types and functions (TypeCat) as forming a large category.

Opposite category, where morphism are reversed.

Call op(::Cat) instead of directly instantiating this type.

Opposite functor, given by the same mapping between opposite categories.

Call op(::Functor) instead of directly instantiating this type.

Abstract base type for a natural transformation between functors.

A natural transformation $α: F ⇒ G$ has a domain $F$ and codomain $G$ (dom and codom), which are functors $F,G: C → D$ having the same domain $C$ and codomain $D$. The transformation consists of a component $αₓ: Fx → Gx$ in $D$ for each object $x ∈ C$, accessible using component or indexing notation (Base.getindex).

Pair of Julia types regarded as a category.

The Julia types should form an @instance of the theory of categories (Theories.Category).

2-cell dual of a 2-category.

Codomain object of natural transformation.

Given $α: F ⇒ G: C → D$, this function returns $D$.

Component of natural transformation.

Domain object of natural transformation.

Given $α: F ⇒ G: C → D$, this function returns $C$.

Evaluate functor on morphism.

Are two morphisms in a category equal?

By default, just checks for equality of Julia objects using $==$. In some categories, checking equality of morphisms may involve nontrivial reasoning.

Evaluate functor on object.

Oppositization 2-functor.

The oppositization endo-2-functor on Cat, sending a category to its opposite, is covariant on objects and morphisms and contravariant on 2-morphisms, i.e., is a 2-functor $op: Catᶜᵒ → Cat$. For more explanation, see the nLab.

Codomain of morphism in category.

Domain of morphism in category.

Coerce or look up morphism in category.

See also: ob.

Coerce or look up object in category.

Converts the input to an object in the category, which should be of type Ob in a category of type Cat{Ob,Hom}. How this works depends on the category, but a common case is to look up objects, which might be integers or GAT expressions, by their human-readable name, usually a symbol.

See also: hom.

Compose morphisms in a category.

Identity morphism on object in category.

2-category of finitely presented categories.

This module is for the 2-category Cat what the module FinSets is for the category Set: a finitary, combinatorial setting where explicit calculations can be carried out. We emphasize that the prefix Fin means "finitely presented," not "finite," as finite categories are too restrictive a notion for many purposes. For example, the free category on a graph is finite if and only if the graph is DAG, which is a fairly special condition. This usage of Fin is also consistent with FinSet because for sets, being finite and being finitely presented are equivalent.

A finitely presented (but not necessarily finite!) category.

Abstract type for category backed by finite generating graph.

Category presented by a finite graph together with path equations.

The objects of the category are vertices in the graph and the morphisms are paths, quotiented by the congruence relation generated by the path equations. See (Spivak, 2014, Category theory for the sciences, §4.5).

Abstract type for category whose morphisms are paths in a graph.

(Or equivalence classes of paths in a graph, but we compute with

Category defined by a Presentation object.

The presentation type can, of course, be a category (Theories.Category). It can also be a schema (Theories.Schema). In this case, the schema's objects and attribute types are regarded as the category's objects and the schema's morphisms, attributes, and attribute types as the category's morphisms (where the attribute types are identity morphisms). When the schema is formalized as a profunctor whose codomain category is discrete, this amounts to taking the collage of the profunctor.

Size of a finitely presented category.

A functor out of a finitely presented category.

Functor out of a finitely presented category given by explicit mappings.

A functor between finitely presented categories.

A natural transformation whose domain category is finitely generated.

This type is for natural transformations $α: F ⇒ G: C → D$ such that the domain category $C$ is finitely generated. Such a natural transformation is given by a finite amount of data (one morphism in $D$ for each generating object of $C$) and its naturality is verified by finitely many equations (one equation for each generating morphism of $C$).

Natural transformation with components given by explicit mapping.

Free category generated by a finite graph.

The objects of the free category are vertices in the graph and the morphisms are (possibly empty) paths.

Path in a graph.

The path is allowed to be empty but always has definite start and end points (source and target vertices).

Collect assignments of functor's morphism map as a vector.

Collect assignments of functor's object map as a vector.

Components of a natural transformation.

Force evaluation of lazily defined function or functor.

Generating graph for a finitely presented category.

Coerce or look up morphism generator in a finitely presented category.

Since morphism generators often have a different data type than morphisms (e.g., in a free category on a graph, the morphism generators are edges and the morphisms are paths), the return type of this function is generally different than that of hom.

Name of morphism generator, if any.

When morphism generators have names, this function is a one-sided inverse to hom_generator. See also: ob_generator_name.

Morphism generators of finitely presented category.

Is the category discrete?

A category is discrete if it is has no non-identity morphisms.

Is the category freely generated?

Is the purported functor on a presented category functorial?

This function checks that functor preserves domains and codomains. When check_equations is true (the default), it also checks that the functor preserves all equations in the domain category. Note that in some cases this may not be possible.

See also: is_natural.

Dual to a final functor, an initial functor is one for which pulling back diagrams along it does not change the limits of these diagrams.

This amounts to checking, for a functor C->D, that, for every object d in Ob(D), the comma category (F/d) is connected.

Is the transformation between FinDomFunctors a natural transformation?

This function uses the fact that to check whether a transformation is natural, it suffices to check the naturality equations on a generating set of morphisms of the domain category. In some cases, checking the equations may be expensive or impossible. When the keyword argument check_equations is false, only the domains and codomains of the components are checked.

See also: is_functorial.

Coerce or look up object generator in a finitely presented category.

Because object generators usually coincide with objects, the default method for ob in finitely presented categories simply calls this function.

Name of object generator, if any.

When object generators have names, this function is a one-sided inverse to ob_generator in that ob_generator(C, ob_generator_name(C, x)) == x.

Object generators of finitely presented category.

The object generators of finite presented category are almost always the same as the objects. In principle, however, it is possible to have equations between objects, so that there are fewer objects than object generators.