# Categorical algebra

## Sets and Relations

The following APIs implement FinSet, the category of Finite Sets (actually the skeleton of FinSet). The objects of this category are natural numbers where `n`

represents a set with `n`

elements. The morphisms are functions between such sets. We use the skeleton of FinSet in order to ensure that all sets are finite and morphisms can be stored using lists of integers. Finite relations are built out of FinSet and can be used to do some relational algebra.

`Catlab.CategoricalAlgebra.Sets`

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

.

`Catlab.CategoricalAlgebra.Sets.ConstantFunction`

— TypeFunction in **Set** taking a constant value.

`Catlab.CategoricalAlgebra.Sets.PredicatedSet`

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

`Catlab.CategoricalAlgebra.Sets.SetFunction`

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

`Catlab.CategoricalAlgebra.Sets.SetOb`

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

.

`Catlab.CategoricalAlgebra.Sets.TypeSet`

— TypeA Julia data type regarded as a set.

`Catlab.Theories.Ob`

— MethodForgetful functor Ob: Cat → Set.

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

`Catlab.CategoricalAlgebra.FinSets`

— ModuleThe category of finite sets and functions, and its skeleton.

`Catlab.CategoricalAlgebra.FinSets.FinDomFunction`

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

`Catlab.CategoricalAlgebra.FinSets.FinFunction`

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

.

`Catlab.CategoricalAlgebra.FinSets.FinSet`

— TypeFinite 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}`

.

`Catlab.CategoricalAlgebra.FinSets.HashJoin`

— TypeHash join algorithm.

`Catlab.CategoricalAlgebra.FinSets.JoinAlgorithm`

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

.

`Catlab.CategoricalAlgebra.FinSets.NestedLoopJoin`

— TypeNested-loop join algorithm.

This is the naive algorithm for computing joins.

`Catlab.CategoricalAlgebra.FinSets.SmartJoin`

— TypeMeta-algorithm for joins that attempts to pick an appropriate algorithm.

`Catlab.CategoricalAlgebra.FinSets.SortMergeJoin`

— TypeSort-merge join algorithm.

`Catlab.CategoricalAlgebra.FinSets.SubFinSet`

— TypeSubset of a finite set.

`Catlab.CategoricalAlgebra.FinSets.SubOpBoolean`

— TypeAlgorithm to compute subobject operations using elementwise boolean logic.

`Catlab.CategoricalAlgebra.FinSets.TabularLimit`

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

`Catlab.CategoricalAlgebra.FinSets.TabularSet`

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

`Catlab.CategoricalAlgebra.FinSets.is_indexed`

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

`Catlab.CategoricalAlgebra.FinSets.preimage`

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

`Catlab.CategoricalAlgebra.FinRelations`

— ModuleThe category of finite sets and relations, and its skeleton.

`Catlab.CategoricalAlgebra.FinRelations.BoolRig`

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

.

`Catlab.CategoricalAlgebra.FinRelations.FinRel`

— TypeObject in the category of finite sets and relations.

See also: `FinSet`

.

`Catlab.CategoricalAlgebra.FinRelations.FinRelation`

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

).

`Catlab.CategoricalAlgebra.FinRelations.FinRelationCallable`

— TypeRelation in FinRel defined by a callable Julia object.

`Catlab.CategoricalAlgebra.FinRelations.FinRelationMatrix`

— TypeRelation in FinRel represented by a boolean matrix.

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

## Free Diagrams, Limits, and Colimts

The following modules define free diagrams in an arbitrary category and specify limit and colimt cones over said diagrams. Thes constructions enjoy the fullest support for FinSet and are used below to define presheaf categories as C-Sets. The general idea of these functions is that you set up a limit computation by specifying a diagram and asking for a limit or colimit cone, which is returned as a struct containing the apex object and the leg morphisms. This cone structure can be queried using the functions `apex`

and `legs`

. Julia's multiple dispatch feature is heavily used to specialize limit and colimit computations for various diagram shapes like product/coproduct and equalizer/coequalizer. As a consumer of this API, it is highly recommended that you use multiple dispatch to specialize your code on the diagram shape whenever possible.

`Catlab.CategoricalAlgebra.FreeDiagrams`

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

`Catlab.CategoricalAlgebra.FreeDiagrams.BipartiteFreeDiagram`

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

`Catlab.CategoricalAlgebra.FreeDiagrams.BipartiteFreeDiagram`

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

`Catlab.CategoricalAlgebra.FreeDiagrams.ComposableMorphisms`

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

.

`Catlab.CategoricalAlgebra.FreeDiagrams.ComposablePair`

— TypePair of composable morphisms in a category.

Composable pairs are a common special case of `ComposableMorphisms`

.

`Catlab.CategoricalAlgebra.FreeDiagrams.Cospan`

— TypeCospan of morphisms in a category.

A common special case of `Multicospan`

. See also `Span`

.

`Catlab.CategoricalAlgebra.FreeDiagrams.DiscreteDiagram`

— TypeDiscrete diagram: a diagram with no non-identity morphisms.

`Catlab.CategoricalAlgebra.FreeDiagrams.FixedShapeFreeDiagram`

— TypeAbstract type for free diagram of fixed shape.

`Catlab.CategoricalAlgebra.FreeDiagrams.Multicospan`

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

`Catlab.CategoricalAlgebra.FreeDiagrams.Multispan`

— Type`Catlab.CategoricalAlgebra.FreeDiagrams.ParallelMorphisms`

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

.

`Catlab.CategoricalAlgebra.FreeDiagrams.ParallelPair`

— TypePair of parallel morphisms in a category.

A common special case of `ParallelMorphisms`

.

`Catlab.CategoricalAlgebra.FreeDiagrams.Span`

— Type`Catlab.CategoricalAlgebra.FreeDiagrams.apex`

— MethodApex of multispan or multicospan.

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

.

`Catlab.CategoricalAlgebra.FreeDiagrams.bundle_legs`

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

`Catlab.CategoricalAlgebra.FreeDiagrams.cocone_objects`

— MethodObjects in diagram that will have explicit legs in colimit cocone.

See also: `cone_objects`

.

`Catlab.CategoricalAlgebra.FreeDiagrams.cone_objects`

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

.

`Catlab.CategoricalAlgebra.FreeDiagrams.diagram_type`

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

`Catlab.CategoricalAlgebra.FreeDiagrams.feet`

— MethodFeet of multispan or multicospan.

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

.

`Catlab.CategoricalAlgebra.FreeDiagrams.legs`

— MethodLegs of multispan or multicospan.

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

`Catlab.Theories.left`

— MethodLeft leg of span or cospan.

`Catlab.Theories.right`

— MethodRight leg of span or cospan.

`Catlab.CategoricalAlgebra.Limits`

— ModuleLimits and colimits in a category.

`Catlab.CategoricalAlgebra.Limits.AbstractColimit`

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

`Catlab.CategoricalAlgebra.Limits.AbstractLimit`

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

`Catlab.CategoricalAlgebra.Limits.Colimit`

— TypeColimit in a category.

`Catlab.CategoricalAlgebra.Limits.ColimitAlgorithm`

— TypeAlgorithm for computing colimits.

`Catlab.CategoricalAlgebra.Limits.ComposeCoproductCoequalizer`

— TypeCompute pushout by composing a coproduct with a coequalizer.

See also: `ComposeProductEqualizer`

.

`Catlab.CategoricalAlgebra.Limits.ComposeProductEqualizer`

— TypeCompute pullback by composing a product with an equalizer.

See also: `ComposeCoproductCoequalizer`

.

`Catlab.CategoricalAlgebra.Limits.Limit`

— TypeLimit in a category.

`Catlab.CategoricalAlgebra.Limits.LimitAlgorithm`

— TypeAlgorithm for computing limits.

`Catlab.CategoricalAlgebra.Limits.SpecializeColimit`

— TypeMeta-algorithm attempting to reduce general colimits to common special cases.

Dual to `SpecializeLimit`

.

`Catlab.CategoricalAlgebra.Limits.SpecializeLimit`

— TypeMeta-algorithm attempting to reduce general limits to common special cases.

Specifically, reduce limits of free diagrams that happen to be discrete to products. TODO: Handle pullbacks similarly.

`Catlab.CategoricalAlgebra.Limits.ToBipartiteColimit`

— TypeCompute a colimit by reducing the diagram to a free bipartite diagram.

`Catlab.CategoricalAlgebra.Limits.ToBipartiteLimit`

— TypeCompute a limit by reducing the diagram to a free bipartite diagram.

`Catlab.CategoricalAlgebra.Limits.can_pushout_complement`

— MethodCan a pushout complement be constructed for a composable pair?

Even in nice categories, this is not generally possible.

`Catlab.CategoricalAlgebra.Limits.colimit`

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

`Catlab.CategoricalAlgebra.Limits.limit`

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

`Catlab.CategoricalAlgebra.Limits.pullback`

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

`Catlab.CategoricalAlgebra.Limits.pushout`

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

`Catlab.CategoricalAlgebra.Limits.pushout_complement`

— MethodPushout complement: extend composable pair to a pushout square.

Pushout complements are the essential ingredient for double pushout (DPO) rewriting.

`Catlab.CategoricalAlgebra.Limits.universal`

— Function`Catlab.Theories.coequalizer`

— MethodCoequalizer of morphisms with common domain and codomain.

To implement for a type `T`

, define the method `colimit(::ParallelPair{T})`

or `colimit(::ParallelMorphisms{T})`

.

`Catlab.Theories.copair`

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

`Catlab.Theories.coproduct`

— MethodCoproduct of objects.

To implement for a type `T`

, define the method `colimit(::ObjectPair{T})`

and/or `colimit(::DiscreteDiagram{T})`

.

`Catlab.Theories.create`

— MethodUnique morphism out of an initial object.

To implement for a type `T`

, define the method `universal(::Initial{T}, ::SMulticospan{0,T})`

.

`Catlab.Theories.delete`

— MethodUnique morphism into a terminal object.

To implement for a type `T`

, define the method `universal(::Terminal{T}, ::SMultispan{0,T})`

.

`Catlab.Theories.equalizer`

— MethodEqualizer of morphisms with common domain and codomain.

To implement for a type `T`

, define the method `limit(::ParallelPair{T})`

and/or `limit(::ParallelMorphisms{T})`

.

`Catlab.Theories.factorize`

— MethodFactor 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})`

.

`Catlab.Theories.initial`

— MethodInitial object.

To implement for a type `T`

, define the method `colimit(::EmptyDiagram{T})`

.

`Catlab.Theories.pair`

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

`Catlab.Theories.product`

— MethodProduct of objects.

To implement for a type `T`

, define the method `limit(::ObjectPair{T})`

and/or `limit(::DiscreteDiagram{T})`

.

`Catlab.Theories.terminal`

— MethodTerminal object.

To implement for a type `T`

, define the method `limit(::EmptyDiagram{T})`

.

`Catlab.CategoricalAlgebra.Limits.@cartesian_monoidal_instance`

— MacroDefine cartesian monoidal structure using limits.

Implements an instance of `CartesianCategory`

assuming that finite products have been implemented following the limits interface.

`Catlab.CategoricalAlgebra.Limits.@cocartesian_monoidal_instance`

— MacroDefine cocartesian monoidal structure using colimits.

Implements an instance of `CocartesianCategory`

assuming that finite coproducts have been implemented following the colimits interface.

## Categories

`Catlab.CategoricalAlgebra.Categories`

— Module2-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 `@instance`

s 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`

.

`Catlab.CategoricalAlgebra.Categories.Cat`

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

.

`Catlab.CategoricalAlgebra.Categories.CompositeFunctor`

— TypeComposite of functors.

`Catlab.CategoricalAlgebra.Categories.Functor`

— TypeAbstract 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 `Cat`

), so when writing generic code one should prefer the `ob_map`

and `hom_map`

functions.

`Catlab.CategoricalAlgebra.Categories.IdentityFunctor`

— TypeIdentity functor on a category.

`Catlab.CategoricalAlgebra.Categories.Transformation`

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

).

`Catlab.CategoricalAlgebra.Categories.TypeCat`

— TypePair of Julia types regarded as a category.

The Julia types should form an `@instance`

of the theory of categories (`Theories.Category`

).

`Catlab.CategoricalAlgebra.Categories.codom_ob`

— MethodCodomain object of natural transformation.

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

`Catlab.CategoricalAlgebra.Categories.component`

— FunctionComponent of natural transformation.

`Catlab.CategoricalAlgebra.Categories.dom_ob`

— MethodDomain object of natural transformation.

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

`Catlab.CategoricalAlgebra.Categories.hom_map`

— MethodEvaluate functor on morphism.

`Catlab.CategoricalAlgebra.Categories.is_hom_equal`

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

`Catlab.CategoricalAlgebra.Categories.ob_map`

— MethodEvaluate functor on object.

`Catlab.Theories.codom`

— MethodCodomain of morphism in category.

`Catlab.Theories.compose`

— MethodCompose morphisms in a category.

`Catlab.Theories.dom`

— MethodDomain of morphism in category.

`Catlab.Theories.hom`

— MethodCoerce or look up morphism in category.

`Catlab.Theories.id`

— MethodIdentity morphism on object in category.

`Catlab.Theories.ob`

— MethodCoerce or look up object in category.

`Catlab.CategoricalAlgebra.FinCats`

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

`Catlab.CategoricalAlgebra.FinCats.FinCat`

— TypeAbstract type for finitely presented category.

`Catlab.CategoricalAlgebra.FinCats.FinCatGraph`

— TypeAbstract type for category backed by finite generating graph.

`Catlab.CategoricalAlgebra.FinCats.FinCatGraphEq`

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

`Catlab.CategoricalAlgebra.FinCats.FinCatPathGraph`

— TypeAbstract type for category whose morphisms are paths in a graph.

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

`Catlab.CategoricalAlgebra.FinCats.FinCatPresentation`

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

`Catlab.CategoricalAlgebra.FinCats.FinDomFunctor`

— TypeA functor out of a finitely presented category.

`Catlab.CategoricalAlgebra.FinCats.FinDomFunctorMap`

— TypeFunctor out of a finitely presented category given by explicit mappings.

`Catlab.CategoricalAlgebra.FinCats.FinFunctor`

— TypeA functor between finitely presented categories.

`Catlab.CategoricalAlgebra.FinCats.FinTransformation`

— TypeA 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$).

`Catlab.CategoricalAlgebra.FinCats.FinTransformationMap`

— TypeNatural transformation with components given by explicit mapping.

`Catlab.CategoricalAlgebra.FinCats.FreeCatGraph`

— TypeFree category generated by a finite graph.

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

`Catlab.CategoricalAlgebra.FinCats.Path`

— TypePath in a graph.

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

`Catlab.CategoricalAlgebra.FinCats.collect_hom`

— MethodCollect assignments of functor's morphism map as a vector.

`Catlab.CategoricalAlgebra.FinCats.collect_ob`

— MethodCollect assignments of functor's object map as a vector.

`Catlab.CategoricalAlgebra.FinCats.components`

— MethodComponents of a natural transformation.

`Catlab.CategoricalAlgebra.FinCats.force`

— MethodForce evaluation of lazily defined function or functor.

`Catlab.CategoricalAlgebra.FinCats.graph`

— MethodGenerating graph for a finitely presented category.

`Catlab.CategoricalAlgebra.FinCats.hom_generators`

— FunctionMorphism generators of finitely presented category.

`Catlab.CategoricalAlgebra.FinCats.is_discrete`

— MethodIs the category discrete?

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

`Catlab.CategoricalAlgebra.FinCats.is_free`

— MethodIs the category freely generated?

`Catlab.CategoricalAlgebra.FinCats.is_functorial`

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

.

`Catlab.CategoricalAlgebra.FinCats.is_natural`

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

.

`Catlab.CategoricalAlgebra.FinCats.ob_generators`

— FunctionObject generators of finitely presented category.

The object generators 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.

## Acsets

### Overview and Theory

For an in depth look into the theory behind acsets, we refer the reader to our paper on the subject, which also gives some sense as to how the implementation works. Here, we give a brief tutorial before the the API documentation.

The most essential part of the acset machinery is the schema. The schema *parameterizes* the acset: each schema corresponds to a different type of acset. Schemas consist of four parts.

- Objects $X,Y$ (
`(X,Y,Z)::Ob`

) - Homomorphisms $f \colon X \to Y$ (
`f :: Hom(X,Y)`

), which go from objects to objects - Attribute types $\mathtt{T}$ (
`T :: AttrType`

) - Attributes $a \colon X \to \mathtt{T}$ (
`a :: Attr(X,T)`

), which go from objects to data types

For those with a categorical background, a schema is a presentation of a category $|S|$ along with a functor $S$ from $|S|$ to the arrow category $0 \to 1$, such that $S^{-1}(1)$ is discrete.

An acset $F$ on a schema consists of...

- a set $F(X)$ of "primary keys" for each object
- a function $F(f) \colon F(X) \to F(Y)$ for each morphism
- a Julia data type $F(\mathtt{T})$ for each data type $\mathtt{T}$
- a function $F(a) \colon F(X) \to F(\mathtt{T})$ for each attribute $a$.

For those with a categorical background, an acset on a schema $S$ consists of a functor from $S$ to $\mathsf{Set}$, such that objects in $S^{-1}(0)$ map to finite sets, and objects in $S^{-1}(1)$ map to sets that represent types. For any particular functor $K \colon S^{-1}(1) \to \mathsf{Set}$, we can also take the category of acsets that restrict to this map on $S^{-1}$.

We can also add relations to this presentation, but we currently do nothing with those relations in the implementation; they mostly serve as documentation.

We will now give an example of how this all works in practice.

```
using Catlab, Catlab.CategoricalAlgebra
# Write down the schema for a weighted graph
@present TheoryWeightedGraph(FreeSchema) begin
V::Ob
E::Ob
src::Hom(E,V)
tgt::Hom(E,V)
T::AttrType
weight::Attr(E,T)
end
# Construct the type used to store acsets on the previous schema
# We *index* src and tgt, which means that we store not only
# the forwards map, but also the backwards map.
@acset_type WeightedGraph(TheoryWeightedGraph, index=[:src,:tgt])
# Construct a weighted graph, with floats as edge weights
g = @acset WeightedGraph{Float64} begin
V = 4
E = 5
src = [1,1,1,2,3]
tgt = [2,3,4,4,4]
weight = [7.2, 9.3, 9.4, 0.1, 42.0]
end
```

E | src | tgt | weight |
---|---|---|---|

1 | 1 | 2 | 7.2 |

2 | 1 | 3 | 9.3 |

3 | 1 | 4 | 9.4 |

4 | 2 | 4 | 0.1 |

5 | 3 | 4 | 42.0 |

### API

We first give an overview of the data types used in the acset machinery.

`FreeSchema`

A finite presentation of a category that will be used as the schema of a database in the *algebraic databases* conception of categorical database theory. Functors out of a schema into FinSet are combinatorial structures over the schema. Attributes in a schema allow you to encode numerical (any julia type) into the database. You can find several examples of schemas in `Catlab.Graphs`

where they define categorical versions of graph theory.

`CSet/AttributedCSet`

is a struct/constructors whose values (tables, indices) are parameterized by a CatDesc/AttrDesc. These are in memory databases over the schema equiped with `ACSetTranformations`

as natural transformations that encode relationships between database instances.

`CSetType/AttributedCSetType`

provides a function to construct a julia type for ACSet instances, parameterized by CatDesc/AttrDesc. This function constructs the new type at runtime. In order to have the interactive nature of Julia, and to dynamically construct schemas based on runtime values, we need to define new Julia types at runtime. This function converts the schema spec to the corresponding Julia type.

`CatDesc/AttrDesc`

the encoding of a schema into a Julia type. These exist because Julia only allows certain kinds of data in the parameter of a dependent type. Thus, we have to serialize a schema into those primitive data types so that we can use them to parameterize the ACSet type over the schema. This is an implementation detail subject to complete overhaul.

`Catlab.CategoricalAlgebra.CSets`

— ModuleCategories of C-sets and attributed C-sets.

`Catlab.CategoricalAlgebra.CSets.ACSetHomomorphismAlgorithm`

— TypeAlgorithm for finding homomorphisms between attributed $C$-sets.

`Catlab.CategoricalAlgebra.CSets.ACSetTransformation`

— TypeTransformation between attributed C-sets.

Homomorphisms of attributed C-sets generalize homomorphisms of C-sets (`CSetTransformation`

), which the user should understand before reading further.

A homomorphism of attributed C-sets with schema S: C ↛ A (a profunctor) is a natural transformation between the corresponding functors col(S) → Set, where col(S) is the collage of S. When the components on attribute types, indexed by objects of A, are all identity functions, the morphism is called *tight*; in general, it is called *loose*. The terms "tight" and "loose" come from what the nLab calls an "M-category". The category of acsets on a fixed schema S is an M-category. Calling `ACSetTransformation`

will construct a tight or loose morphism as appropriate, depending on which components are specified.

Since every tight morphism can be considered a loose one, the distinction between tight and loose may seem an unimportant technicality, but it can have important consequences because choosing one or the other greatly affects limits and colimits of acsets. In practice, the tight morphisms suffice for most purposes, including computing colimits. However, when computing limits of acsets, the loose morphism are usually preferable.

`Catlab.CategoricalAlgebra.CSets.BacktrackingSearch`

— TypeFind attributed $C$-set homomorphisms using backtracking search.

This procedure uses the classic backtracking search algorithm for a combinatorial constraint satisfaction problem (CSP). As is well known, the homomorphism problem for relational databases is reducible to CSP. Since the C-set homomorphism problem is "the same" as the database homomorphism problem (insofar as attributed C-sets are "the same" as relational databases), it is also reducible to CSP. Backtracking search for CSP is described in many computer science textbooks, such as (Russell & Norvig 2010, *Artificial Intelligence*, Third Ed., Chapter 6: Constraint satisfaction problems, esp. Algorithm 6.5). In our implementation, the search tree is ordered using the popular heuristic of "minimum remaining values" (MRV), also known as "most constrained variable.

`Catlab.CategoricalAlgebra.CSets.CSetTransformation`

— TypeTransformation between C-sets.

Recall that a C-set homomorphism is a natural transformation: a transformation between functors C → Set satisfying the naturality axiom for every (generating) morphism in C.

This data type records the data of a C-set transformation. Naturality is not strictly enforced but is expected to be satisfied. It can be checked using the function `is_natural`

.

`Catlab.CategoricalAlgebra.CSets.HomomorphismQuery`

— TypeFind attributed $C$-set homomorphisms using a conjunctive query.

This algorithm evaluates a conjunctive query (limit in `FinSet`

) to find all homomorphisms between two $C$-sets. In fact, conjunctive queries are exactly the *representable* functors from $C$-sets to sets, so every conjunctive query arises in this way, with the caveat that conjunctive queries may correspond to to infinite $C$-sets when $C$ is infinite (but possibly finitely presented).

`Catlab.CategoricalAlgebra.CSets.LooseACSetTransformation`

— TypeLoose transformation between attributed C-sets.

See `ACSetTranformation`

for the distinction between tight and loose.

`Catlab.CategoricalAlgebra.CSets.SubCSet`

— TypeSub-C-set of a C-set.

`Catlab.CategoricalAlgebra.CSets.TightACSetTransformation`

— TypeTight transformation between attributed C-sets.

See `ACSetTranformation`

for the distinction between tight and loose.

`Catlab.ACSetInterface.copy_parts!`

— MethodCopy parts from a set-valued `FinDomFunctor`

to an `ACSet`

.

`Catlab.CategoricalAlgebra.CSets.generate_json_acset`

— MethodSerialize an ACSet object to a JSON string

`Catlab.CategoricalAlgebra.CSets.homomorphism`

— MethodFind a homomorphism between two attributed $C$-sets.

Returns `nothing`

if no homomorphism exists. For many categories $C$, the $C$-set homomorphism problem is NP-complete and thus this procedure generally runs in exponential time. It works best when the domain object is small.

To restrict to *monomorphisms*, or homomorphisms whose components are all injective functions, set the keyword argument `monic=true`

. To restrict only certain components to be injective or bijective, use `monic=[...]`

or `iso=[...]`

. For example, setting `monic=[:V]`

for a graph homomorphism ensures that the vertex map is injective but imposes no constraints on the edge map.

To restrict the homomorphism to a given partial assignment, set the keyword argument `initial`

. For example, to fix the first source vertex to the third target vertex in a graph homomorphism, set `initial=(V=Dict(1 => 3),)`

.

Use the keyword argument `alg`

to set the homomorphism-finding algorithm. By default, a backtracking search algorithm is used (`BacktrackingSearch`

).

See also: `homomorphisms`

, `isomorphism`

.

`Catlab.CategoricalAlgebra.CSets.homomorphisms`

— MethodFind all homomorphisms between two attributed $C$-sets.

This function is at least as expensive as `homomorphism`

and when no homomorphisms exist, it is exactly as expensive.

`Catlab.CategoricalAlgebra.CSets.is_homomorphic`

— MethodIs the first attributed $C$-set homomorphic to the second?

This function generally reduces to `homomorphism`

but certain algorithms may have minor optimizations.

`Catlab.CategoricalAlgebra.CSets.is_isomorphic`

— MethodAre the two attributed $C$-sets isomorphic?

This function generally reduces to `isomorphism`

but certain algorithms may have minor optimizations.

`Catlab.CategoricalAlgebra.CSets.isomorphism`

— MethodFind an isomorphism between two attributed $C$-sets, if one exists.

See `homomorphism`

for more information about the algorithms involved.

`Catlab.CategoricalAlgebra.CSets.isomorphisms`

— MethodFind all isomorphisms between two attributed $C$-sets.

This function is at least as expensive as `isomorphism`

and when no homomorphisms exist, it is exactly as expensive.

`Catlab.CategoricalAlgebra.CSets.parse_json_acset`

— MethodDeserialize a dictionary from a parsed JSON string to an object of the given ACSet type

`Catlab.CategoricalAlgebra.CSets.parse_json_acset`

— MethodDeserialize a JSON string to an object of the given ACSet type

`Catlab.CategoricalAlgebra.CSets.read_json_acset`

— MethodRead a JSON file to an object of the given ACSet type

`Catlab.CategoricalAlgebra.CSets.write_json_acset`

— MethodSerialize an ACSet object to a JSON file

`Catlab.CategoricalAlgebra.StructuredCospans`

— ModuleStructured cospans.

This module provides a generic interface for structured cospans with a concrete implementation for attributed C-sets.

`Catlab.CategoricalAlgebra.StructuredCospans.StructuredCospan`

— TypeStructured cospan.

The first type parameter `L`

encodes a functor L: A → X from the base category `A`

, often FinSet, to a category `X`

with "extra structure." An L-structured cospan is then a cospan in X whose feet are images under L of objects in A. The category X is assumed to have pushouts.

Structured cospans form a double category with no further assumptions on the functor L. To obtain a symmetric monoidal double category, L must preserve finite coproducts. In practice, L usually has a right adjoint R: X → A, which implies that L preserves all finite colimits. It also allows structured cospans to be constructed more conveniently from an object x in X plus a cospan in A with apex R(x).

See also: `StructuredMulticospan`

.

`Catlab.CategoricalAlgebra.StructuredCospans.StructuredCospan`

— MethodConstruct structured cospan in R-form.

`Catlab.CategoricalAlgebra.StructuredCospans.StructuredCospan`

— MethodConstruct structured cospan in L-form.

`Catlab.CategoricalAlgebra.StructuredCospans.StructuredCospanOb`

— TypeObject in the category of L-structured cospans.

`Catlab.CategoricalAlgebra.StructuredCospans.StructuredMulticospan`

— TypeStructured multicospan.

A structured multicospan is like a structured cospan except that it may have a number of legs different than two.

See also: `StructuredCospan`

.

`Catlab.CategoricalAlgebra.StructuredCospans.StructuredMulticospan`

— MethodConstruct structured multicospan in R-form.

`Catlab.CategoricalAlgebra.StructuredCospans.OpenACSetTypes`

— MethodCreate types for open attributed C-sets from an attributed C-set type.

Note: the type passed in should *not* be instantiated with concrete attribute types.

The resulting types, for objects and morphisms, each have the same type parameters for data types as the original type.

See also: `OpenCSetTypes`

.

`Catlab.CategoricalAlgebra.StructuredCospans.OpenCSetTypes`

— MethodCreate types for open C-sets from a C-set type.

Returns two types, for objects, a subtype of `StructuredCospanOb`

, and for morphisms, a subtype of `StructuredMulticospan`

.

See also: `OpenACSetTypes`

.

`Catlab.ACSetInterface.acset_schema`

— FunctionGet the schema of an acset at runtime.

`Catlab.ACSetInterface.add_part!`

— MethodAdd part of given type to acset, optionally setting its subparts.

Returns the ID of the added part.

See also: `add_parts!`

.

`Catlab.ACSetInterface.add_parts!`

— FunctionAdd parts of given type to acset, optionally setting their subparts.

Returns the range of IDs for the added parts.

See also: `add_part!`

.

`Catlab.ACSetInterface.copy_parts!`

— FunctionCopy parts from a C-set to a C′-set.

The selected parts must belong to both schemas. All subparts common to the selected parts, including data attributes, are preserved. Thus, if the selected parts form a sub-C-set, then the whole sub-C-set is preserved. On the other hand, if the selected parts do *not* form a sub-C-set, then some copied parts will have undefined subparts.

TODO: handle colons

`Catlab.ACSetInterface.copy_parts_only!`

— FunctionCopy parts from a C-set to a C′-set, ignoring all non-data subparts.

The selected parts must belong to both schemas. Attributes common to both schemas are also copied, but no other subparts are copied.

See also: `copy_parts!`

.

`Catlab.ACSetInterface.has_part`

— FunctionWhether an acset has a part with the given name.

`Catlab.ACSetInterface.incident`

— FunctionGet superparts incident to part in acset.

If the subpart is indexed, this takes constant time; otherwise, it takes linear time. As with `subpart`

, both single and vectorized access, as well as chained access, are supported. Note that sequences of morphisms are supplied in the usual left-to-right order, so that

`incident(g, x, [:src, :vattr])`

returns the list of all edges whose source vertex has vertex attribute `x`

.

Note that when the subpart is indexed, this function returns a view of the underlying index, which should not be mutated. To ensure that a fresh copy is returned, regardless of whether indexing is enabled, set the keyword argument `copy=true`

.

`Catlab.ACSetInterface.nparts`

— FunctionNumber of parts of given type in an acset.

`Catlab.ACSetInterface.parts`

— MethodParts of given type in an acset.

`Catlab.ACSetInterface.rem_part!`

— FunctionRemove part from a C-set.

The part is removed using the "pop and swap" strategy familiar from LightGraphs.jl, where the "removed" part is actually replaced by the last part, which is then deleted. This strategy has important performance benefits since only the last part must be assigned a new ID, as opposed to assigning new IDs to *every* part following the removed part.

The removal operation is *not* recursive. When a part is deleted, any superparts incident to it are retained, but their subparts become undefined (equal to the integer zero). For example, in a graph, if you call `rem_part!`

on a vertex, the edges incident the `src`

and/or `tgt`

vertices of the edge become undefined but the edge itself is not deleted.

Indexing has both positive and negative impacts on performance. On the one hand, indexing reduces the cost of finding affected superparts from linear time to constant time. On the other hand, the indices of subparts must be updated when the part is removed. For example, in a graph, indexing `src`

and `tgt`

makes removing vertices faster but removing edges (slightly) slower.

See also: `rem_parts!`

.

`Catlab.ACSetInterface.rem_parts!`

— MethodRemove parts from a C-set.

The parts must be supplied in sorted order, without duplicates.

See also: `rem_part!`

.

`Catlab.ACSetInterface.set_subpart!`

— FunctionMutate subpart of a part in a C-set.

Both single and vectorized assignment are supported.

See also: `set_subparts!`

.

`Catlab.ACSetInterface.set_subparts!`

— MethodMutate subparts of a part in a C-set.

Both single and vectorized assignment are supported.

See also: `set_subpart!`

.

`Catlab.ACSetInterface.subpart`

— FunctionGet subpart of part in acset.

Both single and vectorized access are supported, with a view of the underlying data being returned in the latter case. Chaining, or composition, of subparts is also supported. For example, given a vertex-attributed graph `g`

,

`subpart(g, e, [:src, :vattr])`

returns the vertex attribute of the source vertex of the edge `e`

. As a shorthand, subparts can also be accessed by indexing:

`g[e, :src] == subpart(g, e, :src)`

Be warned that indexing with lists of subparts works just like `subpart`

: `g[e,[:src,:vattr]]`

is equivalent to `subpart(g, e, [:src,:vattr])`

. This convention differs from DataFrames but note that the alternative interpretation of `[:src,:vattr]`

as two independent columns does not even make sense, since they have different domains (belong to different tables).

`Catlab.ACSetInterface.tables`

— FunctionGet a named tuple of Tables.jl-compatible tables from an acset