Theory and Applications of Categories, Vol. 32, No. 16, 2017, pp. 547–619.

ALGEBRAIC DATABASES

PATRICK SCHULTZ, DAVID I. SPIVAK, CHRISTINA VASILAKOPOULOU, AND RYAN WISNESKY

Abstract. Databases have been studied category-theoretically for decades. While mathematically elegant, previous categorical models have typically struggled with representing concrete data such as integers or strings.

In the present work, we propose an extension of the earlier set-valued functor model, making use of multi-sorted algebraic theories (a.k.a. Lawvere theories) to incorporate concrete data in a principled way. This approach easily handles missing information (null values), and also allows constraints and queries to make use of operations on data, such as multiplication or comparison of numbers, helping to bridge the gap between traditional databases and programming languages.

We also show how all of the components of our model — including schemas, instances, change-of-schema functors, and queries — fit into a single double categorical structure called a proarrow equipment (a.k.a. framed bicategory).

Contents

1 Introduction  548
2 Profunctors and proarrow equipments  551
3 Algebraic theories  565
4 Presentations and syntax  567
5 Algebraic database schemas  577
6 Algebraic database instances  582
7 The fundamental data migration functors  587
8 The double category �ata  593
9 Queries and uber-queries  608
10 Implementation  612
A Componentwise composition and exponentiation in �ata  615

Schultz, Spivak, and Vasilakopoulou were supported by AFOSR grant FA9550–14–1–0031, ONR grant N000141310260, and NASA grant NNL14AA05C. Wisnesky was supported by NIST SBIR grant 70NANB15H290.

Received by the editors 2016-02-10 and, in final form, 2017-04-24. Transmitted by Richard Blute. Published on 2017-04-27. 2010 Mathematics Subject Classification: 18C10, 18D05, 68P15. Key words and phrases: Databases, algebraic theories, proarrow equipments, collage construction,

data migration.

\begin{matrix}c \\ ◯ \end{matrix} Patrick Schultz, David I. Spivak, Christina Vasilakopoulou, and Ryan Wisnesky, 2017. Permission to copy for private use granted.

1. Introduction

Category-theoretic models of databases have been present for some time. For example in [RW92; FGR03; JR02] databases schemas are formalized as sketches of various sorts (e.g. EA sketches = finite limits + coproducts). The data itself (called an instance) is represented by a model of the sketch. In this language, queries can be understood as limit cones in such a sketch. While different from the traditional relational foundations of database theory [AHV95], this is in general a very natural and appealing idea.

In [Spi12], Spivak puts emphasis on the ability to move data from one format, or database schema, to another. To enable that, he proposes defining schemas to be mere categories — or in other words trivial sketches (with no (co)limit cones). A schema morphism is just a functor. Unlike the case for non-trivial sketches, a schema morphism induces three adjoint functors, the pullback and its Kan extensions. These functors can be called data migration functors because they transfer data from one schema to another. In this formalism, queries can be recovered as specific kinds of data migration.

Both of the above approaches give some secondary consideration to attributes, e.g. the name or salary of an employee, taking values in some data type, such as strings, integers, or booleans. Rosebrugh et al. formalized attributes in terms of infinite coproducts of a chosen terminal object, whereas Spivak formalized them by slicing the category of copresheaves over a fixed object. However, neither approach seemed to work convincingly in implementations [SW15].

1.1. The approach of this paper. In the present paper, the goal of providing a principled and workable formalization of attributes is a central concern. We consider attribute values as living in an algebra over a multi-sorted algebraic theory, capturing operations such as comparing integers or concatenating strings. A database schema is formalized as what we call an algebraic profunctor, which is a profunctor from a category to an algebraic theory that preserves the products of the theory. Each element of the profunctor represents an observation of a given type (string, integer, boolean) that can be made on a certain entity (employee, department). For example, if an entity has an observable for length and width, and if the theory has a multiplication, then the entity has an observable for area.

We also focus on providing syntax for algebraic databases. We can present a schema, or an instance on it, using a set of generators and relations. The generators act like the “labelled nulls” used in modern relational databases, easily handling unknown information, while the relations are able to record constraints on missing data. In this sense, our approach can be related to knowledge bases or ontologies [MS08]. One can express that Pablo is an employee whose salary is between 65 and 75, and deduce various facts; for example, if the schema expresses that each employee’s salary is at most that of his or her manager, one can deduce that Pablo’s manager makes at least 65.

Mathematically, this paper develops the theory of algebraic profunctors. An algebraic profunctor can be regarded as a diagram of models for an algebraic theory �, e.g. a presheaf of rings or modules on a space. Algebraic profunctors to a fixed � form the objects in a proarrow equipment — a double category satisfying a certain fibrancy condition — which we call �ata. This double category includes database schemas and schema morphisms, and we show that the horizontal morphisms (which we call bimodules between schemas) generalize both instances and conjunctive queries.

We make heavy use of collages of profunctors and bimodules. Collages are a kind of double-categorical colimit which have been studied in various guises under various names — [GS15] gives a good general treatment. We propose exactness properties which the collage construction satisfies in some examples; we say that an equipment has extensive collages when these properties hold. This fits in with the work started in [Sch15], and may be of interest independent of the applications in this paper. Although the present work only makes use of the properties of extensive collages in the equipment �rof of categories, functors, and profunctors, we found more direct proofs of these properties in this case to be no easier and less illuminating.

To connect the theory with practice, it is necessary to have a concrete syntax for presenting the various categorical structures of interest. While it is mostly standard, we provide a self-contained account of a type-theoretic syntax for categories, functors, profunctors, algebraic theories, algebras over those theories, and algebraic profunctors. We use this syntax to consistently ground the theoretical development with concrete examples in the context of databases, though the reader need not have any background in that subject.

1.2. Implementation. The mathematical framework developed in this paper is implemented in an open-source software system we call OPL, available for download at http://categoricaldata.net/fql.html. All examples from this paper are included as built-in demonstrations in the OPL tool. We defer a detailed discussion of OPL until the end of the paper (Section 10), but two high-level introductory remarks are in order.

First, we note that most constructions on finitely-presented categories require solving word problems in categories and hence are not computable [FGR03]. Given a category presented by generators G and relations (equations) E, the word problem asks if two terms (words) in G are equal under E. Although not decidable in general, many approaches to this problem have been proposed; we discuss our particular approach in Section 10. If we can solve the word problem for a particular category presentation, then we can use that decision procedure to implement query evaluation, construct collages, and perform other tasks.

Second, we note that there are many connections between the mathematical framework presented here and various non-categorical frameworks. When restricted to a discrete algebraic theory, the query language we discuss in Section 9 corresponds exactly to relational algebra’s unions of conjunctive queries under bag semantics [SW15]. This correspondence allows fragments of our framework to be efficiently implemented using existing relational systems (MySQL, Oracle, etc), and our software has indeed been used on various real-world examples [Wis+15].

1.3. Outline. In Section 2 we review profunctors and use them to motivate the definition of double categories and proarrow equipments. We also review, as well as refine, the notion of collages, which exist in all of the equipments of interest in this paper. In Section 3 we review multisorted algebraic theories, and we discuss profunctors — from categories to algebraic theories — that preserve products in the appropriate way; we call these algebraic profunctors. We save relevant database-style examples until Section 4, where we provide type-theoretic syntax for presenting theories, categories and (algebraic) profunctors. This section serves as a foundation for the syntax used throughout the paper, especially in examples, though it can be skipped by those who only want to understand the category theoretic concepts.

We get to the heart of the new material in Section 5 and Section 6, where we define schemas and instances for algebraic databases and give examples. Morphisms between schemas induce three adjoint functors — called data migration functors — between their instance categories, and we discuss this in Section 7.

In Section 8 we wrap all of this into a double category (in fact a proarrow equipment) �ata, in which schemas are objects, schema morphisms are vertical morphisms, and schema bimodules — defined in this section — are horizontal morphisms. Instances are shown to be bimodules of a special sort, and the data migration functors from the previous section are shown to be obtained by composition and exponentiation of instance bimodules with representable bimodules. In this way, we see that �ata nicely packages all of the structures and operations of interest.

Finally, in Section 9 we discuss the well-known "Select-From-Where" queries of standard database languages and show that they form a very special case of our data migration setup. We conclude with a discussion of the implementation of our mathematical framework in Section 10.

1.4. Notation. In this paper we will adhere to the following notation. For named categories, such as the category Set of sets, we use bold roman. For category variables — for instance "Let � be a category" — we use math script.

Named bicategories or 2-categories, such as the 2-category 𝒞at of small categories, will be denoted similarly to named 1-categories except with calligraphic first letter. We use the same notation for a variable bicategory ℬ .

Double categories, such as the double category �rof of categories, functors, and profunctors, will be denoted like 1-categories except with blackboard bold first letter. We use the same notation for a variable double category �.

If � and � are categories, we sometimes denote the functor category 𝒞at(�, �) by [�, �] or �^{�} .

1.5. Acknowledgements. The authors thank the anonymous referee for many helpful and questions and comments.

2. Profunctors and proarrow equipments

We begin with a review of profunctors, which are sometimes called correspondences or distributors; standard references include [Bor94a] and [Bén00]. Together with categories and functors, these fit into a proarrow equipment in the sense of Wood [Woo82; Woo85], though we follow the formulation in terms of double categories called framed bicategories (or fibrant double categories), due to Shulman [Shu08; Shu10]. Eventually, in Section 8, we will produce an equipment �ata that encompasses database schemas, morphisms, instances, and queries.

2.1. Profunctors. Perhaps the most important example of an equipment is that of categories, functors, and profunctors. We review profunctors here, as they will be a central player in our story.

Let � and � be categories. Recall that a profunctor M from � to �, written M: � �, is defined to be a functor M: �^{op} × � → Set.

2.2. Profunctors as matrices. It can be helpful to think of profunctors as something like matrices. Given finite sets X and Y, there is an equivalence between

• X × Y -matrices A (i.e. functions X × Y → �),

• functions A: X → �^{Y},

• functions A: Y → �^{X},

• linear maps L_{A}: �^{X} → �^{Y},

• linear maps L′_{A}: �^{Y} → �^{X}. Similarly, there is an equivalence between

• profunctors M: � �,

• functors M: �^{op} → Set^{�} ,

• functors M: � → Set^{�^{op}} ,

• colimit-preserving functors Λ_{M}: Set^{�} → Set^{�} ,

• colimit-preserving functors Λ′_{M}: Set^{�^{op}} → Set^{�^{op}} . The first three correspondences are straightforward by the cartesian monoidal closed structure of Cat. The last two follow from the fact that, just as �^{Y} is the free real vector space on the set Y, the category Set^{�^{op}} is the free completion of � under colimits, and similarly for Set^{�} . By the equivalence between colimit-preserving functors Set^{�} → � and functors �^{op} → � for any cocomplete category �, the functor Λ_{M} is obtained by taking the left Kan extension of M: �^{op} → Set^{�} along the Yoneda embedding y: �^{op} → Set^{�} . Using the pointwise formula for Kan extensions, this means that given any I: � → Set, the functor Λ_{M}(I): � → Set is given by the coend formula

(Λ_{M}I)(d) = ∫ ^{c∈�} I(c) × M(c, d).  (1)

This is analogous to the matrix formula (L_{A}v)_{y} = ∑_{x∈X} v_{x}A_{x,y}.

Alternatively, since colimits in Set^{�} are computed pointwise, we can express Λ_{M}I itself as a coend in Set^{�}

Λ_{M}I = ∫ ^{c∈�} I(c) · M(c)  (2)

where we think of M as a functor �^{op} → Set^{�} . The symbol · represents the settheoretic copower (see [Kel05]), i.e. I(c)·M(c) is an I(c)-fold coproduct of copies of M(c). Formula (2) is analogous to the matrix formula L_{A}v = ∑_{x∈X} A(x)v_{x}, where we think of A as a function X → �^{Y} and A(x)v_{x} denotes scalar multiplication by v_{x} ∈ �. The construction of Λ′_{M} is very similar.

2.3. Profunctors as bimodules. One can also think of a profunctor as a sort of graded bimodule: for each pair of objects c ∈ � and d ∈ � there is a set M(c, d) of elements in the bimodule, and given an element m ∈ M(c, d) and morphisms f: c′ → c in � and g: d → d′ in �, there are elements g · m ∈ M(c, d′) and m · f ∈ M(c′, d), such that the equations (g · m) · f = g · (m · f), g′ · (g · m) = (g′ ∘ g) · m, and (m · f) · f′ = m · (f ∘ f′) hold whenever they make sense.

2.4. Representable profunctors. Profunctors also act as generalized functors, just like relations R ⊆ A × B act as generalized functions A → B. Any functor F: � → � induces profunctors �(F, −): � � and �(−, F): � �, called the profunctors represented by F. These profunctors are defined by

�(F, −)(c, d) := �(F c, d) �(−, F)(d, c) := �(d, F c).  (3)

2.5. Tensor product of profunctors. Given two profunctors

�  �  � M N

there is a tensor product M ⊙ N: � �, given by the coend formula

(M ⊙ N)(c, e) = ∫ ^{d∈�} M(c, d) × N(d, e).  (4)

Following Section 2.2, this is analogous to matrix multiplication: (AB)_{i,k} = ∑_{j} A_{i,j}B_{j,k}. Equivalently, (M ⊙ N)(c, e) is the coequalizer of the diagram

∐_{d_{1},d_{2}∈�} M(c, d_{1}) × �(d_{1}, d_{2}) × N(d_{2}, e)∐_{d∈�} M(c, d) × N(d, e) (5)

where the two maps are given by the right action of � on M and by the left action of � on N. In the notation of Section 2.3, we can write elements of (M ⊙ N)(c, e) as tensors m ⊗ n, where m ∈ M(c, d) and n ∈ N(d, e) for some d ∈ �. The coequalizer then implies that (m · f) ⊗ n = m ⊗ (f · n) whenever the equation makes sense. Notice the similarity to the tensor product of bimodules over rings.

Alternatively, we can define the tensor product by the composition

M ⊙ N = �^{op} ⟶^{M} Set^{�} ⟶^{Λ_{N}} Set^{�},

or by the composition Λ′_{N} ∘ M: � → Set^{�^{op}}. This is clearly equivalent to (4), using (1).

For any category �, there is a profunctor Hom_{�} : �^{op} × � → Set, which we will often write as � = Hom_{�} when unambiguous. For any functors F: � → Set and G: �^{op} → Set, there are natural isomorphisms

∫ ^{c∈�} F (c) × �(c, c′) ≅ F (c′)  ∫ ^{c∈�} �(c′, c) × G(c) ≅ G(c′),  (6)

a result sometimes referred to as the coYoneda lemma [Kel05, (3.71)]. Continuing with the analogy from Section 2.2, Hom_{�} acts like an identity matrix: ∑_{i} δ_{i,j}v_{i} = v_{j}. That is, these hom profunctors act as units for the tensor product, since (6) shows that Hom_{�} ⊙M ≅ M ≅ M ⊙ Hom_{�} . Following Section 2.3, one can think of Hom_{�} as the regular (�, �)- bimodule, i.e. as � acting on itself on both sides [Mat89].

2.6. Profunctor morphisms. A morphism ϕ: M ⇒ N between two profunctors

\begin{aligned}& � & �, \\ M \\ N \end{aligned}

is defined to be a natural transformation between the set-valued functors. In other words, for each c ∈ � and d ∈ � there is a component function ϕ_{c,d}: M(c, d) → N(c, d) such that the equation ϕ(f · m · g) = f · ϕ(m) · g holds whenever it makes sense.

Categories, profunctors, and profunctor morphisms form a bicategory 𝒫 rof. To explain how functors fit in, we need to discuss proarrow equipments.

2.7. Proarrow equipments. Before going into more properties of profunctors, it will be useful to put them in a more general and abstract framework. A double category is a 2-category-like structure involving two types of 1-cell — horizontal and vertical — as well as 2-cells. A proarrow equipment (which we typically abbreviate to just equipment) is a double category satisfying a certain fibrancy condition. An excellent reference is the paper [Shu08], where they are called framed bicategories.

We will see in Example 2.12 that there is an equipment �rof whose objects are categories, whose vertical 1-cells are functors, and whose horizontal 1-cells are profunctors. This is the motivating example to keep in mind for equipments. In Section 8 we will define �ata, the other main proarrow equipment of the paper, whose objects are database schemas.

2.8. Definition. A double category � consists of the following data:

• A category �_{0}, which we refer to as the vertical category of �. For any two objects A, B ∈ �_{0}, we will write �_{0}(A, B) for the set of vertical arrows from A to B. We refer to objects of �_{0} as objects of �.

• A category �_{1}, equipped with two functors L, R: �_{1} → �_{0}, called the left frame and right frame functors. Given an object M ∈ Ob �_{1} with A = L(M) and B = R(M), we say that M is a proarrow (or horizontal arrow) from A to B and write M: A B. A morphism ϕ: M → N in �_{1} is called a 2-cell, and is drawn as follows, where f = L(ϕ) and g = R(ϕ):

\begin{matrix}A & B \\ C & D \end{matrix} ; M ; f ; g ; N ; ⇓ϕ  (7)

• A unit functor U: �_{0} → �_{1}, which is a section of both L and R, i.e. L ∘ U = id_{�_{0}} = R ∘ U. We will often write U_{A} or even A for the unit proarrow, U(A): A A, and similarly U_{f} of just f for U(f).

• A functor ⊙: �_{1} ×_{�_{0}} �_{1} → �_{1}, called horizontal composition, that is weakly associative and weakly unital in the sense that there are coherent unitor and associator isomorphisms. See [Shu08] for details.

Given a double category �, we will sometimes write Vert(�) for the vertical category �_{0}. There is also a horizontal bicategory, denoted ℋ (�), whose objects and 1-cells are the objects and horizontal 1-cells of �, and whose 2-cells are the 2-cells of � of the form (7) such that f = id_{A} and g = id_{B}.

Given f, g, M, N as in (7), we write _{f}�_{g}(M, N) for the set of 2-cells from M to N with frames f and g, and write ℋ (�)(M, N) for the case where f and g are identity morphisms. If A and B are objects, then �(A, B) will always mean the set of vertical arrows from A to B, where ℋ (�)(A, B) is used when we want the category of proarrows.

We follow the convention of writing horizontal composition serially, i.e. the horizontal composite of proarrows M: A B and N: B C, is M ⊙ N: A C.

2.9. Definition. A double category � is right closed [resp. left closed] when its horizontal bicategory is, i.e. when composing a proarrow N [resp. M] with an arbitrary proarrow, (− ⊙ N), [resp. (M ⊙ −)] has a left adjoint. Following [Shu08], we denote this left adjoint by (N ▷ −) [resp. by (− ◁ M)]; hence there are bijections

ℋ (�)(X ⊙ N, P) ≅ ℋ (�)(X, N ▷ P)
ℋ (�)(M ⊙ X, P) ≅ ℋ (�)(X, P ◁ M)

natural in X and P. � is biclosed when both adjoints exist.

Recall from [Bor94b] the definitions of cartesian morphisms and fibrations of categories.

2.10. Definition. A proarrow equipment (or just equipment) is a double category � in which the frame functor

(L, R): �_{1} → �_{0} × �_{0}

is a fibration. If f: A → C and g: B → D are vertical morphisms and N: C D is a proarrow, a cartesian morphism M → N in �_{1} over (f, g) is a 2-cell

\begin{matrix}A & B \\ C & D \end{matrix} M f g N ⇓cart

which we call a cartesian 2-cell. We refer to M as the restriction of N along f and g, written M = N(f, g).

Equivalently, an equipment is a double category in which every vertical arrow f: A → B has a companion f̂: A B and a conjoint f̂: B A, together with 2-cells satisfying certain equations (see [Shu08]). In this view, the canonical cartesian lifting of some proarrow N along (f, g) is given by N(f, g) ≅ f̂⊙ N ⊙ ĝ.

2.11. Adjunction between representable proarrows. Any vertical morphism in an equipment � induces an adjunction f̂ ⊣ f̂ in the horizontal bicategory ℋ (�), with unit denoted η_{f} and counit denoted ϵ_{f}. Moreover, the following bijective correspondences hold for any vertical morphisms f: A → B, g: C → D, and proarrows M: A B, N: C D:

\begin{aligned}_{f}�_{g}(M, N) & ≅ ℋ (�)(M, f̂⊙ N ⊙ ĝ) \\ & ≅ ℋ (�)(M ⊙ ĝ, f̂⊙ N) \\ & ≅ ℋ (�)(f̂ ⊙ M, N ⊙ ĝ) \\ & ≅ ℋ (�)(f̂ ⊙ M ⊙ ĝ, N). \end{aligned}  (8)

The last bijection shows that in an equipment, the frame functor (L, R): �_{1} → �_{0} × �_{0} turns out to also be an opfibration.

We record some notation for (8). Given a 2-cell ϕ ∈ _{f}�_{g}(M, N), we write ϕ̂ ∈ ℋ (�)(M ⊙ ĝ, f̂ ⊙ N) and ϕ̂ ∈ ℋ (�)(f̂ ⊙ M, N ⊙ ĝ) for its image under the above bijections,

\begin{matrix}A & B \\ C & D \end{matrix} ; M ; f ; g ; N ; ⇓ϕ  \begin{matrix}A & B & D \\ A & C & D \end{matrix} M ĝ f̂ N ⇓ϕ̂  \begin{matrix}C & A & B \\ C & D & B \end{matrix} f̂ M N ĝ ⇓ϕ̂

2.12. Example. There is a double category �rof defined as follows. The vertical category is �rof_{0} = Cat the category of small categories and functors. Given objects �, � ∈ �rof, a horizontal arrow between them is a profunctor M: � �, as described in Section 2.1. A 2-cell ϕ ∈ _{F} �rof_{G}(M, N), as to the left of (9), denotes a natural transformation, as to the right of (9), with components ϕ_{c,d}: M(c, d) → N(F c, Gd):

�  � �  � ; M ; F ; G ; N ; ⇓ϕ  \begin{aligned}�^{op} × � & & �^{op} × � \\ & Set \end{aligned} M F^{op}×G ⇒^{ϕ} N (9)

The horizontal composite of profunctors M ⊙N is defined by the coend (4), or equivalently by the coequalizer (5), and the horizontal unit is U_{�} = Hom_{�} : � �. This gives �rof the structure of a double category, such that ℋ (�rof) is the bicategory 𝒫 rof defined in Section 2.6.

Moreover, the double category �rof is biclosed (see Definition 2.9): given proarrows M: � �, N: � �, and P: � �, one defines left and right exponentiation using ends

(N ▷ P)(c, d) = ∫_{e∈�} P (c, e)^{N(d,e)} = [�, Set](N(d, −), P (c, −))
(P ◁ M)(d, e) = ∫_{c∈�} P (c, e)^{M(c,d)} = [�^{op}, Set](M(−, d), P (−, e))

which evidently inherit left and right actions from the respective categories when viewed as bimodules.

Finally, �rof is an equipment because for any F, G, N as in (9), there is a cartesian 2-cell whose domain is precisely the profunctor N(F, G) := N ∘ (F^{op} × G) obtained by composition. The companion and conjoint of any functor F: � → � are the representable profunctors (3)

F̂ = �(F, −) and F̂ = �(−, F).

Thus we can also represent the cartesian lifting as N(F, G) = F̂ ⊙ N ⊙ Ĝ.

2.13. Definition. Let � be a small category. We say that a double category � has local colimits of shape � if, for each pair of objects A, B ∈ �, the hom-category ℋ (�)(A, B) has colimits of shape � and these are preserved by horizontal composition on both sides,

L ⊙ (colim_{i∈�} M_{i}) ≅ colim_{i∈�} (L ⊙ M_{i})
(colim_{i∈�} M_{i}) ⊙ N ≅ colim_{i∈�} (M_{i} ⊙ N).

We say that � has local colimits if it has local colimits of shape � for all small � .

2.14. Example. The equipment �rof has local colimits. Indeed, each horizontal bicategory is a category of set-valued functors. Colimits exist, and they are preserved by horizontal composition because composition is defined by coends, which are themselves colimits.

2.15. Collage of a proarrow. In some equipments �, a proarrow can be represented in a certain sense by an object in �, called its collage. For example, it is well known that a profunctor can be represented by a category, as we review in Example 2.19. In this section we collect some useful properties of the collage construction, in an arbitrary equipment.

We note briefly that the collage construction was also studied in [Woo85], in a slightly different setting. The definition we give below of an equipment with extensive collages is somewhat more general than the set of axioms considered in [Woo85], as we don’t require the existence of Kleisli objects for (horizontal) monads.

2.16. Definition. Let M: A B be a proarrow in an equipment �. Its collage is an object M̃ equipped with vertical arrows i_{A}: A → M̃ ← B :i_{B}, called the collage inclusions, together with a 2-cell

\begin{matrix}A & B \\ M̃ & M̃, \end{matrix} M i_{A} i_{B} M̃ ⇓μ  (10)

that is universal in the sense that any diagram as to the left below (a cocone under M) factors uniquely as to the right:

\begin{matrix}A & B \\ X & X \end{matrix} ; M ; f_{A} ; f_{B} ; X ; ⇓f =  \begin{matrix}A & B \\ M̃ & M̃ \\ X & X \end{matrix} M i_{A} i_{B} M̃ f̄ f̄ X ⇓μ ⇓f̄  (11)

2.17. Remark. The existence of a 2-cell μ with the above universal property amounts to the existence of a left adjoint ˜(−): �_{1} → �_{0} to the unit functor U from Definition 2.8, since it establishes a bijection �_{0}(M̃, X) ≅ �_{1}(M, U_{X}). From this perspective, the universal 2-cell μ : M ⇒ UM̃, as in (10), is the unit of the adjunction.

2.18. Definition. An equipment � is said to have collages if every proarrow in � has a collage as in (11). By Remark 2.17, � has collages if and only if there exists a left adjoint ˜(−): �_{1} → �_{0} to the unit functor U.

We say � has normal collages if additionally the unit of the adjunction μ is cartesian.

2.19. Example. The proarrow equipment �rof has normal collages. The collage M̃ of a profunctor M: �^{op} × � → Set is a category where Ob(M̃) := Ob(�) ⊔ Ob(�), and

M̃(x, y) = \begin{cases}�(x, y) & if x ∈ � and y ∈ � \\ M(x, y) & if x ∈ � and y ∈ � \\ ∅ & if x ∈ � and y ∈ � \\ �(x, y) & if x ∈ � and y ∈ � \end{cases}  (12)

Composition in M̃ is defined using composition in � and � and the functoriality of M. There are evident functors i_{�} : � → M̃ and i_{�} : � → M̃, and the 2-cell μ: M ⇒ UM̃ sends an element m ∈ M(c, d) to m ∈ M̃(i_{�} (c), i_{�} (d)) = M(c, d). It is easy to see that μ is cartesian, so �rof has normal collages.

This construction satisfies the universal property (11). Suppose we are given f_{�} : � → �, f_{�} : � → �, and a 2-cell f as in (11). It is easy to see that the unique f̄: M̃ → � (and so Uf̄: UM̃ ⇒ U_{�} ) that works is defined by cases, using f_{�} on objects and morphisms in �, using f_{�} on objects and morphisms in �, and using f on morphisms with domain in � and codomain in �.

Note also that for any profunctor M as above, there is an induced functor M̃ → 2, where 2 = {0 → 1}, sometimes called the free arrow category, is the collage of the terminal profunctor {∗} {∗}. In fact, if Cat/2 denotes the slice category, it is not hard to check that the collage construction provides an equivalence of categories

�rof_{1} ≃ Cat/2  (13)

In particular, from a functor F: � → 2 we obtain a profunctor between the pullbacks of F along 0, 1: {∗} → 2 respectively.

2.20. Proarrows between collages; simplices. We now want to consider general proarrows M̃ Ñ between collages in �, by defining a category of simplices. Although we will only need this in the case � = �rof, we found the proofs simpler in the general case.

For intuition, consider two profunctors M: �_{0} �_{1} and N: �_{0} �_{1}. A profunctor X: M̃ Ñ must assign a set X(c, d) in four different cases: c is an object in either �_{0} or �_{1}, and likewise for d. We could try splitting X into four profunctors X_{i,j}: �_{i} �_{j}, but this would not encode all of the functorial actions needed to recover X. For instance, given objects c ∈ �_{0}, c′ ∈ �_{1}, and d ∈ �_{0}, and given an element x ∈ X_{1,0}(c′, d) and a morphism m: c → c′ in M̃ (i.e. an element m ∈ M(c, c′)), there is an element m · x ∈ X_{0,0}(c, d). The idea behind the following construction is to encode all of the data of a profunctor X between collage objects by four profunctors, together with four 2-cells which capture all of those functorial actions.

2.21. Definition. Let M: A_{0} A_{1} and N: B_{0} B_{1} be proarrows in �. We define an (M, N)-simplex X to be a collection of proarrows {X_{0,0}, X_{0,1}, X_{1,0}, X_{1,1}}

\begin{matrix}A_{1} & B_{0} \\ A_{0} & B_{1} \end{matrix} X_{1,0} X_{1,1} N X_{0,0} X_{0,1} M

together with four 2-cells X_{0,∗}, X_{1,∗}, X_{∗,0}, X_{∗,1} as in

\begin{aligned}A_{1} \\ & B_{k} \\ A_{0} \end{aligned} ; X_{1,k} ; M ; X_{0,k} ; ⇓X_{∗,k}  \begin{aligned}& B_{0} \\ A_{j} \\ & B_{1} \end{aligned} ; N ; X_{j,0} ; X_{j,1} ; ⇓X_{j,∗}

such that the following equation holds:

\begin{matrix}A_{1} & B_{0} \\ A_{0} & B_{1} \end{matrix} ; X_{1,0} ; N ; X_{0,0} ; X_{0,1} ; M ; ⇓X_{∗,0} ; ⇓X_{0,∗} =  \begin{matrix}A_{1} & B_{0} \\ A_{0} & B_{1} \end{matrix} ; X_{1,0} ; X_{1,1} ; N ; X_{0,1} ; M ; ⇓X_{1,∗} ; ⇓X_{∗,1}

A morphism α: X → Y between two (M, N)-simplices consists of component 2-cells α = (α_{0,0}, α_{0,1}, α_{1,0}, α_{1,1}), where α_{j,k}: X_{j,k} → Y_{j,k} satisfy four evident equations. We have thus defined the category of (M, N)-simplices, denoted _{M}Simp_{N}.

Suppose that the equipment � has local initial objects; see Definition 2.13. Then for any proarrow M: A_{0} A_{1}, there is an (M, M)-simplex given by the proarrows

\begin{matrix}A_{1} & A_{0} \\ A_{0} & A_{1} \end{matrix} ; 0 ; A_{1} ; M ; A_{0} ; M ; M  (14)

together with the evident 2-cells; we call this the unit simplex on M and denote it by 1_{M} ∈ _{M}Simp_{M}.

2.22. The functor _{M}Res_{N}. There is a functor _{M}Res_{N}: ℋ (�)(M̃, Ñ) → _{M}Simp_{N} defined as follows. On some P: M̃ Ñ, the four proarrows are given by the restrictions along the collage inclusions i_{A_{j}}: A_{j} → M̃ and i_{B_{k}}: B_{k} → Ñ, namely X_{j,k} = î_{A_{j}} ⊙ P ⊙ î_{B_{k}}, and the 2-cells are given by horizontal composition with the universal μ_{M}, μ_{N}.

The following proposition follows directly from definitions.

2.23. Proposition. Suppose that � has local initial objects and collages. The four 2cells

\begin{matrix}A & A \\ M̃ & M̃ \end{matrix} A i_{A} i_{A} M̃ ⇓i_{A}  \begin{matrix}A & B \\ M̃ & M̃ \end{matrix} M i_{A} i_{B} M̃ ⇓μ  \begin{matrix}B & A \\ M̃ & M̃ \end{matrix} 0 i_{B} i_{A} M̃ ⇓!  \begin{matrix}B & B \\ M̃ & M̃ \end{matrix} B i_{B} i_{B} M̃ ⇓i_{B}  (15)

induce a morphism u_{M}: 1_{M} → _{M}Res_{M}(UM̃) in _{M}Simp_{M} by unique factorization through cartesian 2-cells. The following are equivalent

1. u_{M} is an isomorphism in _{M}Simp_{M}.

2. each of the four squares in (15) is cartesian.

3. the four induced 2-cells are isomorphisms:

η_{i_{A}}: U_{A} \underrightarrow{∼} î_{A} ⊙ î_{A}, μ: M \underrightarrow{∼} î_{A} ⊙ î_{B}, !: 0 \underrightarrow{∼} î_{B} ⊙ î_{A}, η_{i_{B}}: U_{B} \underrightarrow{∼} î_{B} ⊙ î_{B}. (16)

Note that if � satisfies the equivalent conditions in Proposition 2.23 then, in particular, it has normal collages.

2.24. Definition. Let � be an equipment. We will say that � has extensive collages if it satisfies the following conditions:

1. � has collages and local initial objects,

2. any of the equivalent conditions from Proposition 2.23 are satisfied,

3. for every pair of proarrows M and N, the functor_{M}Res_{N}: ℋ (�)(M̃, Ñ) → _{M}Simp_{N} is an equivalence of categories.

Extensive collages are best behaved in the presence of local finite colimits. The following proposition provides a condition which is equivalent to condition 3 above in this case, but which is often easier to verify. The proof provides an explicit construction of the inverse of _{M}Res_{N} using colimits in the horizontal bicategories.

2.25. Proposition. Suppose that � is an equipment with collages, that it satisfies condition 2 in Definition 2.24, and that � has local finite colimits (so it also satisfies condition 1). Then condition 3 is equivalent to the following condition:

3’. for any proarrow M: A B, the following square is a pushout in ℋ (�)(M̃, M̃):

\begin{matrix}î_{A} ⊙ î_{A} ⊙ î_{B} ⊙ î_{B} & î_{B} ⊙ î_{B} \\ î_{A} ⊙ î_{A} & UM̃ \end{matrix} ; ϵ_{i_{A}}⊙î_{B}⊙î_{B} ; î_{A}⊙î_{A}⊙ϵ_{i_{B}} ; ϵ_{i_{B}} ; ϵ_{i_{A}} ; ⌜ (17)

Proof. Suppose � has local finite colimits and satisfies condition 2. First assuming condition 3 we will show that (17) is a pushout. It suffices that its image under the equivalence _{M}Res_{N} (Section 2.22) is a pushout, i.e. each of the four restriction functors,

î_{A} ⊙ – ⊙ î_{A}: ℋ (�)(M̃, M̃) → ℋ (�)(A, A),

as well as î_{A} ⊙ – ⊙ î_{B}, î_{B} ⊙ – ⊙ î_{A}, and î_{B} ⊙ – ⊙ î_{B}, take the diagram (17) to a pushout square. This follows easily from condition 2, in particular the four isomorphisms of (16).

Conversely, assuming condition 3’, we will show that _{M}Res_{N} is an equivalence of categories for any pair of proarrows M: A_{0} A_{1}, N: B_{0} B_{1}. To define the inverse functor, let X ∈ _{M}Simp_{N} be a simplex, and consider the diagram

\begin{aligned}& A_{1} & B_{0} \\ M̃ & & & Ñ \\ & A_{0} & B_{1} \end{aligned} X_{1,0} X_{1,1} N î_{B0} î_{A1} î_{A0} X_{0,0} X_{0,1} M î_{B1}

which also contains six 2-cells:

X_{∗,k}: M ⊙ X_{1,k} → X_{0,k}, X_{j,∗}: X_{j,0} ⊙ N → X_{j,1},
μ̂_{M}: î_{A_{0}} ⊙ M → î_{A_{1}}, μ̂_{N}: N ⊙ î_{B_{1}} → î_{B_{0}}

where the μ’s are universal 2-cells and μ̂ and μ̂ are as in Section 2.11.

The inverse to _{M}Res_{N}, which we denote (X ↦ X̃): _{M}Simp_{N} → ℋ (�)(M̃, Ñ), is given by sending the simplex X to the colimit in ℋ (�)(M̃, Ñ) of the 3 × 3 square: ^{1}

\begin{matrix}î_{A_{0}}X_{0,0}î_{B_{0}} & î_{A_{0}}MX_{1,0}î_{B_{0}} & î_{A_{1}}X_{1,0}î_{B_{0}} & P î_{B_{0}}î_{B_{0}} \\ î_{A_{0}}X_{0,0}Nî_{B_{1}} & î_{A_{0}}MX_{1,0}Nî_{B_{1}} & î_{A_{1}}X_{1,0}Nî_{B_{1}} & P î_{B_{0}}Nî_{B_{1}} \\ î_{A_{0}}X_{0,1}î_{B_{1}} & î_{A_{0}}MX_{1,1}î_{B_{1}} & î_{A_{1}}X_{1,1}î_{B_{1}} & P î_{B_{1}}î_{B_{1}} \\ î_{A_{0}}î_{A_{0}}P & î_{A_{0}}Mî_{A_{1}}P & î_{A_{1}}î_{A_{1}}P & P \end{matrix} ; X_{∗,0} ; μ̂_{M} ; μ̂_{N} ; X_{0,∗} ; μ̂_{N} ; X_{1,∗} ; X_{∗,0} ; μ̂_{M} ; μ̂_{N} ; X_{1,∗} ; μ̂_{N} ; μ̂_{N} ; X_{∗,1} ; μ̂_{M} ; μ̂_{M} ; μ̂_{M} (18)

Note that this colimit can be formed by first taking the pushout of each row, and then taking the pushout of the resulting span, or by taking column-wise pushouts first. For the time being, ignore the separated right-hand column and bottom row of (18).

1We suppress the ⊙ symbol in the objects to reduce the required space.

We now show that _{M}Res_{N} and X ↦ X̃ are inverse equivalences. Suppose P: M̃ Ñ is a proarrow and let X = _{M}Res_{N}(P); we want to show that there is a natural isomorphism P ≅ X̃. Performing the substitution X_{j,k} = î_{A_{j}}P î_{B_{k}} and using the isomorphisms from (16), e.g. M ≅ î_{A_{0}}î_{A_{1}}, each row (resp. each column) can be seen as a composition of some proarrow — namely the one in the right-hand column (resp. bottom row) — with the diagram (17). Since local colimits commute with proarrow composition, the righthand column (resp. bottom row) proarrows are indeed the pushouts. In the same way, one checks that P is the colimit of both the right-hand column and the bottom row.

In the other direction, if X ∈ _{M}Simp_{N} is any simplex and X̃ is the colimit of the square in (18), we want to show that _{M}Res_{N}(X̃) ≅ X. It is straightforward to check that î_{A_{j}} ⊙ X̃ ⊙ î_{B_{k}} ≅ X_{j,k} by composing the square with î_{A_{j}} on the left and î_{B_{k}} on the right and applying the equations of (16). It is moreover easy to see that these isomorphisms form the components of an isomorphism of simplices _{M}Res_{N}(X̃) ≅ X. Thus _{M}Res_{N} is an equivalence of categories.

2.26. Remark. It is likely possible to characterize equipments with extensive collages (assuming local finite colimits) in terms of an adjunction of double categories. We won’t pursue this further here, but for the interested reader we provide a rough sketch as a starting point for further investigation.

If � is an equipment with local finite colimits, one can define an equipment �imp(�) whose vertical category is �_{1} and whose horizontal 1-cells are simplices. The composition in �imp(�) is given by (51). There is a double functor U: � → �imp(�) sending each object A ∈ � to the unit proarrow U_{A} and each proarrow M: A B to the unit simplex 1_{M} defined in (14).

If � has extensive collages, then U has a left adjoint Col sending each proarrow M ∈ �imp(�) to its collage Col(M) and acting on simplices by the pushout (18). Looking at the definition Definition 2.24, it seems that condition 1 is related to the existence of a left adjoint to U, condition 2 is related to the property that the 2-cell components of the unit of this double-adjunction are cartesian, and condition 3’ is related to the property that the right adjoint Col is normal (preserves unit proarrows). Perhaps this observation can be worked into an equivalent characterization of equipments with extensive collages, but we leave it to the motivated reader to investigate further.

2.27. Example. The equipment �rof has extensive collages. Indeed, �rof has local colimits by Example 2.14 and normal collages by Example 2.19. Moreover, we will verify that �rof satisfies condition 3’ of Proposition 2.25.

If M: � � is a profunctor, then we need to show that (17) is a pushout in the category [M̃^{op} × M̃, Set]. It suffices to show that it is a pointwise pushout. For any objects x, y ∈ M̃, it is not hard to see that (17) becomes one of the following pushout squares in Set:

\begin{matrix}0 & 0 & M(x, y) & M(x, y) \\ �(x, y) & �(x, y) & M(x, y) & M(x, y) \\ 0 & 0 & 0 & �(x, y) \\ 0 & 0 & 0 & �(x, y) \end{matrix} y ∈ � y ∈ � x ∈ � ⌜ ⌜ x ∈ � ⌜ ⌜

2.28. Collages as lax (co)limits. When an equipment � has extensive collages and local finite colimits (like �rof), there is another universal property involving collages, which can be expressed entirely in terms of the horizontal bicategory ℋ (�).

2.29. Definition. Let ℬ be a bicategory, let F: A → B be a 1-cell in ℬ , and let X be an object in ℬ . Define a category of lax cocones from F to X, written _{F} Cocone_{X}, as follows: an object of _{F} Cocone_{X} is a diagram

\begin{aligned}B \\ & X \\ A \end{aligned} P_{B} F P_{A} ⇓π

and a morphism α: (P_{A}, P_{B}, π) → (Q_{A}, Q_{B}, χ) is a pair of 2-cells α_{A}: P_{A} → Q_{A} and α_{B}: P_{B} → Q_{B} making an evident diagram commute.

Any cocone (P_{A}, P_{B}, π) ∈ _{F} Cocone_{X} induces a functor ℬ (X, Y) → _{F} Cocone_{Y} by composition. If this functor is an equivalence of categories, then we say that X is a lax colimit of the arrow F (see for example [Kel89]). Dually, there is a category _{X}Cone_{F} of lax cones from X to F, employed in the definition of lax limits of arrows.

2.30. Proposition. Let � be an equipment with extensive collages and local finite colimits, and let M: A B be a proarrow with collage i_{A}: A → M̃ ← B :i_{B}. The triangle on the left exhibits M̃ as a lax colimit of the 1-cell M in ℋ (�), and the triangle on the right exhibits M̃ as a lax limit of M.

B ; M̃ ; A î_{B} M î_{A} ⇓μ̂  A ; M̃ ; B M î_{A} î_{B} ⇓μ̂

Proof. The 2-cells μ̂, μ̂ correspond to the cartesian μ as in Section 2.11. We will show that the triangle on the left is a lax colimit cocone, i.e. that composing with μ̂ induces an equivalence of categories ℋ (�)(M̃, Y) → _{M}Cocone_{Y} for any Y. We define the inverse functor to send a cocone (P_{A}, P_{B}, π) to the proarrow P: M̃ Y defined by a pushout in ℋ (�)(M̃, Y):

\begin{matrix}î_{A} ⊙ M ⊙ P_{B} & î_{B} ⊙ P_{B} \\ î_{A} ⊙ P_{A} & P \end{matrix} μ̂⊙P_{B} î_{A}⊙π ⌜  (19)

Suppose we start with an arbitrary proarrow Q: M̃ Y, and compose with μ̂ to get the cocone π = μ̂ ⊙ Q: M ⊙ î_{B} ⊙ Q → î_{A} ⊙ Q. We can see that the pushout (19) is just (17) composed by Q on the right, showing P ≅ Q. On the other hand, if we start with an arbitrary cocone π, take the pushout P as in (19), then compose on the left with μ̂: M ⊙ î_{B} → î_{A}, it is easy to check that we get π back.

Thus the pushout (19) does define an inverse functor _{M}Cocone_{Y} → ℋ (�)(M̃, Y), showing that the triangle on the left is a lax colimit cocone. The lax limit cone follows by a dual argument.

2.31. Remark. A converse to Proposition 2.30 holds: if � has local finite colimits such that the conclusion to Proposition 2.30 holds for all proarrows M: A B in �, then � has extensive collages. We won’t need this converse, and so do not prove it. The proof is straightforward, regarding a simplex as a “lax cocone of lax cones” (or visa-versa).

2.32. Remark. For convenience, we will break down the universal property of M̃ as the lax limit of M. Suppose � has extensive collages.

Given any P_{A}: X A, P_{B}: X B, and 2-cell π: P_{A}⊙M → P_{B}, there is a proarrow P: X M̃ (which is unique up to isomorphism by the 2-dimensional part of the universal property of Proposition 2.30) such that π ≅ P ⊙ μ̂. Namely cartesian 2-cells exist, by P_{A} ≅ P ⊙ î_{A}, P_{B} ≅ P ⊙ î_{B}, satisfying the equation (where μ is also cartesian)

\begin{matrix}X & A & B \\ X & M̃ & M̃ \end{matrix} P_{A} M i_{A} i_{B} P M̃ cart ⇓μ  =  \begin{aligned}& A \\ X & & B \\ X & & M̃ \end{aligned} ; M ; P_{A} ; P_{B} ; i_{B} ; P ; ⇓π ; cart (20)

The 2-dimensional part of the universal property says that, given α_{A}: p_{A} → q_{A} and α_{B}: p_{B} → q_{B} such that α_{B} ∘ p = q ∘ α_{A}, there is a unique α: P → Q making the evident diagrams commute.

The universal property for the lax colimit is dual.

3. Algebraic theories

In this section, we recall some basic aspects of the well-known work on algebraic theories and their algebras [ARV11] relevant to our purposes. In particular, algebraic theories are often used to define data types within various programming languages [Mit96], and as stated in the introduction, our main goal is to connect databases and programming languages.

3.1. Definition. A ( multisorted) algebraic theory is a cartesian strict monoidal category � together with a set S_{�}, elements of which are called base sorts, such that the monoid of objects of � is free on S_{�}. The terminal object in � is denoted 1.

The category ATh has algebraic theories as objects, and morphisms � → �′ are product preserving functors F which send base sorts to base sorts: for any s ∈ S_{�}, F (s) ∈ S_{�′}.

3.2. Remark. Throughout this paper we will discuss algebraic theories—categories with finite products and functors that preserve them—which are closely related to the notion of finite product sketches; see [BW85]. However, aside from issues of syntax and computation, everything we say in this paper would also hold if algebraic theories were replaced by essentially algebraic theories—categories with finite limits and functors that preserve them—which are analogous to finite limit sketches.

3.3. Definition. Let � be an algebraic theory. An algebra (sometimes called a model) of � is a finite product-preserving functor � → Set. The category �-Alg of �-algebras is the full subcategory of [�, Set] spanned by the finite product-preserving functors.

3.4. Example. If � is an algebraic theory, and t ∈ � is an object, then the representable functor �(t, −) preserves finite products. Thus the Yoneda embedding y: �^{op} → [�, Set] factors through �-Alg.

In particular, y(1) = �(1, −) is the initial �-algebra for any algebraic theory, called the algebra of constants and denoted by κ := y(1).

We state the following theorem for future reference; proofs can be found in [AR94].

3.5. Theorem. Let � be any algebraic theory.

• The Yoneda embedding y: �^{op} → �-Alg is dense. (By definition, �-Alg is a full subcategory of [�, Set].)

• �-Alg is closed in [�, Set] under sifted colimits. ([AR94, Prop. 2.5].)

• �-Alg has all colimits. ([AR94, Thm. 4.5].)

3.6. Warning. Note that the forgetful functor �-Alg → [�, Set] in general does not preserve colimits; i.e. colimits in �-Alg are not taken pointwise. However, see Remark 6.9.

3.7. Remark. For convenience, we will recall the notion of a dense functor, though we only use it in the case of the inclusion of a full subcategory. A functor F: � → � is dense if one of the following equivalent conditions holds:

• for any object C ∈ �, the canonical cocone from the canonical diagram (F ↓ C) → � to C is a colimit cocone, • the identity functor id_{�} is the pointwise left Kan extension of F along itself,

• the representable functor �(F, −): � → [�^{op}, Set] is fully faithful,

• (assuming � is cocomplete) for any object C ∈ �, the canonical morphism ∫^{A∈�} �(F (A), C) · F (A) → C is an isomorphism.

3.8. Algebraic profunctors. In the previous section, we recalled the basic elements of the theory of profunctors (see Sections 2.1 to 2.6). At this point, we wish to characterize those profunctors between a category and an algebraic theory M: � �, which interact nicely with the products in �.

The following equivalences are easy to establish, by translating a product-preserving condition for M: �^{op} × � → Set under (− × �) ⊣ (−)^{�} , and by (12) for the collage construction in �rof.

3.9. Lemma. Let � be a category and � an algebraic theory. For any profunctor M: � �, the following are equivalent:

• for each c ∈ �, the functor M(c, –): � → Set preserves finite products,

• M: � → Set^{�^{op}} preserves finite products,

• M: �^{op} → Set^{�} factors through the full subcategory �-Alg,

• the inclusion i_{�} : � → M̃ into the collage of M preserves finite products.

3.10. Definition. We refer to a profunctor M satisfying any of the equivalent conditions of Lemma 3.9 as an algebraic profunctor, or we say that it preserves products on the right. We denote a profunctor M: � � which is algebraic, using a differently-decorated arrow

M: � �.

We define the category Prof^{×} to be the full subcategory of the pullback

Prof^{×}  ·  �rof_{1}

Cat × ATh  Cat × Cat

⌟

(L,R)

spanned by the algebraic profunctors. Here, L and R are the frame functors (Definition 2.8).

Suppose given a pair of composable profunctors � ^{M} � ^{N} � in which the latter is algebraic. We want to compose them in such a way that the composition is also algebraic. It is not hard to see that ordinary profunctor composition M ⊙ N does not generally satisfy this property; however, we can define a composition which does. In Definition 3.11 we will formalize this as a left action ⊗ of �rof on Prof^{×}:

Cat  Prof^{×}  ATh

�rof_{1}  ·

Cat  Prof^{×}

L R R L ⊗

⌜

L R

(21)

We thus aim to define a functor ⊗ (dotted line) from the category of composable profunctor pairs where the second is algebraic, such that the above diagram commutes.

Let � be a category, � an algebraic theory, and N: � � an algebraic profunctor. By Lemma 3.9, we can consider N to be a functor N: �^{op} → �-Alg. Define the functor Λ_{N}^{×}: Set^{�} → �-Alg by the coend formula

Λ_{N}^{×}(J) = ∫ ^{d∈�} J(d) · N(d)

taken in the category �-Alg. This coend exists because �-Alg is cocomplete, and the formula coincides with (2), except there the coend is taken in Set^{�}, thus is pointwise.

3.11. Definition. Let M ∈ �rof_{1}(�, �) be a profunctor, and let N ∈ Prof^{×}(�, �) be an algebraic profunctor. The left tensor of M on N, denoted M ⊗ N ∈ Prof^{×}(�, �) is defined by the composition Λ_{N}^{×} ∘ M: �^{op} → �-Alg.

This left tensor can evidently be extended to a functor ⊗ as in (21). It is also simple to check that it defines a left action of �rof on Prof^{×}, in the sense that ⊗ respects units and composition in �rof.

4. Presentations and syntax

In this section we will introduce syntax for algebraic theories, as well as for categories and (co)presheaves. In general, a presentation of a given mathematical object consists of generators and relations in a specified form. The object itself is then obtained by recursively generating terms according to a syntax, and then quotienting by the relations.

The material in this section is relatively standard (see, e.g. [Jac99] or [Mit96]). We go through it carefully in order to fix the notation we will use in examples.

4.1. Presentations of algebraic theories. The presentation of an algebraic theory, as defined in Definition 3.1, does not explicitly mention products. Instead, it relies on multi-arity function symbols on the base sorts. A signature simply lays out these sorts and function symbols.

4.2. Definition. An algebraic signature is a pair Σ = (S_{Σ}, Φ_{Σ}), where S_{Σ} is a set of base sorts and Φ_{Σ} is a set of function symbols. Each function symbol f ∈ Φ is assigned a (possibly empty, ordered) list of sorts dom(f) and a single sort cod(f). We use the notation f: (s_{1}, …, s_{n}) → s′ to mean that dom(f) = (s_{1}, …, s_{n}) and cod(f) = s′. We call n the arity of f; if n = 0, we say it is 0-ary and write it f: () → s′.

4.3. Definition. Let ASig denote the category of algebraic signatures. A morphism F: Σ → Σ′ between signatures is a pair of functions F_{S}: S_{Σ} → S_{Σ′} and F_{Φ} : Φ_{Σ} → Φ_{Σ′}, such that for any function symbol f ∈ Φ_{Σ} with f: (s_{1}, …, s_{n}) → s′, dom(F_{Φ}f) = (F_{S}(s_{1}), …, F_{S}(s_{n})) and cod(F_{Φ}f) = F_{S}(s′).

4.4. Example. Consider the signature Σ for the algebraic theory of monoid actions on a set. There are two sorts, S = {m, s}, and three function symbols, η: () → m for the unit, μ: (m, m) → m for the multiplication, and α: (m, s) → s for the action. If Σ′ is the signature for the theory of monoids, there is an evident inclusion morphism Σ′ → Σ.

4.5. Example. Every algebraic theory � has an underlying algebraic signature Σ_{�}, whose base sorts are those of �, and whose function symbols f: (s_{1}, …, s_{n}) → s′ are the morphisms f ∈ �(s_{1} × ⋯ × s_{n}, s′). This defines a functor U: ATh → ASig.

We will see in Remark 4.14 that U has a left adjoint, giving the free algebraic theory generated by a signature. We construct this left adjoint syntactically, and we will make use of this syntax throughout the paper.

4.6. Definition. Fix an algebraic signature Σ. A context Γ over Σ is formally a set Γ_{v} together with a function Γ_{s}: Γ_{v} → S_{Σ}. In other words, a context is an object of the slice category Set_{/S_{Σ}}, or equivalently the functor category Set^{S_{Σ}}, regarding S_{Σ} as a discrete category. When the set Γ_{v} is finite, we will encode both Γ_{v} and Γ_{s} as a list Γ = (x_{1} : s_{1}, …, x_{n} : s_{n}), and refer to Γ as a finite context.

If Γ = (x_{1} : s_{1}, …, x_{n} : s_{n}) and Γ′ = (x′_{1} : s′_{1}, …, x′_{m} : s′_{m}) are two contexts, we will write Γ, Γ′ = (x_{1} : s_{1}, …, x_{n} : s_{n}, x′_{1} : s′_{1}, …, x′_{m} : s′_{m}) for their concatenation, equivalently given by the induced function Γ_{v} ⊔ Γ′_{v} → S_{Σ}. In practice, when concatenating contexts, we implicitly assume that variables are renamed as necessary to avoid name clashes. We denote the empty context by ∅.

4.7. Remark. Intuitively, a context (x_{1} : s_{1}, …, x_{n} : s_{n}) represents the declaration that symbol x_{i} “belongs to the sort” s_{i}. We treat the parentheses around a context as optional, and use them only as an aid to readability.

The primary role of contexts is to explicitly list the “free variables” which are allowed to be used inside an expression. Thus a context (x : Int, y : A) roughly corresponds to the English “let x be an integer and let y be an element of A”. The next definition makes this intuition precise.

4.8. Definition. Fix an algebraic signature Σ and a context Γ. A term in context Γ is an expression built out of the variables in Γ and function symbols in Σ. Every term has an associated sort. We use the notation Γ ⊢ t : s to denote that t is a term in context Γ and that t has sort s.

Terms in context Γ are defined recursively as follows:

• if (x : s) ∈ Γ, then Γ ⊢ x : s,

• if f: (s_{1}, …, s_{n}) → s′ is a function symbol in Σ and Γ ⊢ t_{i} : s_{i} for each 1 ≤ i ≤ n, then Γ ⊢ f(t_{1}, …, t_{n}) : s′.

We will sometimes refer to terms ∅ ⊢ t in the empty context as ground terms. A ground term t must not contain any variables, and so must be constructed entirely out of function symbols in Σ (which includes 0-ary function symbols). Note that there can be terms in non-empty contexts which contain no variables, but we will not call these ground terms.

4.9. Example. In Example 4.4 we gave the signature Σ for monoid actions. An example term is x_{1} : m, x_{2} : m, p : s ⊢ α(μ(x_{1}, x_{2}), p) : s. An example ground term is ∅ ⊢ μ(η, μ(η, η)) : m.

One can think of a variable x which appears in a term t as a placeholder which can be replaced by other expressions. For instance, in x^{3} − 2x, the variable x can be replaced by any number, or even another polynomial. To make this precise, the operation of substitution is defined recursively.

4.10. Definition. Let Θ, Γ, and Ψ be contexts. If (Θ, x : s, Ψ) ⊢ t : s′ and Γ ⊢ u : s are terms, then Θ, Γ, Ψ ⊢ t[x := u] : s′ denotes the term obtained by replacing all occurrences of x in t with u. This substitution operation is defined formally by recursion:

• x[x := u] = u,

• x′[x := u] = x′ if x′ ≠ x,

• f(t_{1}, …, t_{n})[x := u] = f(t_{1}[x := u], …, t_{n}[x := u]).

If (Θ, x_{1} : s_{1}, …, x_{n} : s_{n}, Ψ) ⊢ t : s′ and Γ ⊢ u_{i} : s_{i} for all 1 ≤ i ≤ n, let Θ, Γ, Ψ ⊢ t[x_{1} := u_{1}, …, x_{n} := u_{n}] : s′ denote the term obtained by simultaneous substitution, also written t[x_{i} := u_{i}] or t[x⃗ := u⃗] for compactness when this is clear.

4.11. Definition. Let Γ and Θ be contexts over an algebraic signature Σ, where Θ = (x_{1} : s_{1}, …, x_{n} : s_{n}) is finite. A context morphism Γ → Θ is a tuple of terms Γ ⊢ t_{i} : s_{i} for 1 ≤ i ≤ n, written [x_{1} := t_{1}, …, x_{n} := t_{n}]: Γ → Θ, or [x_{i} := t_{i}] or [x⃗ := t⃗] for compactness.

If Ψ = (y_{1} : s′_{1}, …, y_{m} : s′_{m}) is another finite context, and [y⃗ := u⃗]: Θ → Ψ a context morphism, the composition [y⃗ := u⃗] ∘ [x⃗ := t⃗] is defined to be [y_{i} := u_{i}[x⃗ := t⃗]]: Γ → Ψ.

4.12. Example. Continuing with Examples 4.4 and 4.9, consider contexts Γ = (x_{1} : m, x_{2} : m, p : s) and Θ = (y : m, q : s). There is a context morphism Γ → Θ given by

[y := x_{1}, q := α(μ(x_{1}, x_{2}), p)] .

4.13. Definition. Let Σ be an algebraic signature. Define the category of contexts over Σ, denoted Cxt_{Σ}, to be the category of finite contexts over Σ and context morphisms. We define the category of possibly infinite contexts over Σ, denoted \overline{Cxt_{Σ}}, to be the obvious extension.

4.14. Remark. It is not hard to see that Cxt_{Σ} has finite products, given by concatenation of contexts, and that the objects of Cxt_{Σ} are freely generated under products by the base sorts (i.e. the singleton contexts). Thus this construction defines a functor Cxt : ASig → ATh. In fact, the functor Cxt is left adjoint to the underlying signature functor U: ATh → ASig from Example 4.5. Hence we will also refer to Cxt_{Σ} as the free algebraic theory on the signature Σ.

The category ASig is for many purposes too rigid: a morphism in ASig is required to send function symbols to function symbols, whereas one often wants to send function symbols to a more complex expression. We now define this more flexible category of signatures.

4.15. Definition. Define ASig^{∗} to be the Kleisli category of the monad induced by the adjunction Cxt ⊣ U of Remark 4.14 on the category ASig.^{2} Concretely, ASig^{∗} is defined just like ASig in Definition 4.3, but where a morphism F: Σ → Σ′ between signatures is allowed to send a function symbol f: (s_{1}, …, s_{n}) → s′ in Φ_{Σ} to an arbitrary term (x_{1} : F_{S}(s_{1}), …, x_{n} : F_{S}(s_{n})) ⊢ F_{Φ}(f) : F_{S}(s′) over Σ′. Composition of these signature morphisms is defined by substitution.

We are now ready to discuss presentations of algebraic theories. We begin with a careful consideration of equations.

4.16. Definition. Let Σ be an algebraic signature. An equation over Σ is a pair of terms (t, t′), where t and t′ are in the same finite context Γ and have the same sort s. We denote such a pair by the equation Γ ⊢ (t = t′) : s, or simply by Γ ⊢ t = t′ if no confusion should arise.

Let E be a set of equations over Σ. Define ≈_{E} to be the smallest equivalence relation on terms over Σ such that

1. if Γ ⊢ t = t′ is an equation of E, then Γ ⊢ t ≈_{E} t′,

2. if f: (s_{1}, …, s_{n}) → s′ is a function symbol and Γ ⊢ (t_{i} ≈_{E} t′_{i}) : s_{i} for all 1 ≤ i ≤ n, then Γ ⊢ (f(t_{1}, …, t_{n}) ≈ f(t′_{1}, …, t′_{n})) : s′,

3. if Θ ⊢ (t ≈_{E} t′) : s, and [x⃗ := u⃗]: Γ → Θ is a context morphism, then Γ ⊢ (t[x⃗ := u⃗] ≈_{E} t′[x⃗ := u⃗]) : s.

4.17. Remark. Condition 3 of Definition 4.16 is equivalent to the following two conditions:

3a. if (Θ, Ψ) ⊢ (t ≈_{E} t′) : s′, then (Θ, x : s, Ψ) ⊢ (t ≈_{E} t′) : s′ for any sort s′, 3b. if (Θ, x : s, Ψ) ⊢ (t ≈_{E} t′) : s′, and Γ ⊢ u : s is a term, then we have (Θ, Γ, Ψ) ⊢

(t[x := u] ≈_{E} t′[x := u]) : s′.

2 We use the symbol ⊢ between contexts and terms; we use the symbol ⊣ for adjunctions. Both are standard notation and no confusion should arise.

4.18. Definition. Let Σ be an algebraic signature, and E a set of equations over Σ. The algebraic theory Cxt_{Σ}/E is the quotient of Cxt_{Σ} by the equivalence relation ≈_{E}. In other words, the objects of Cxt_{Σ}/E are finite contexts over Σ, and the morphisms are ≈_{E}-equivalence classes of context morphisms. This quotient is well defined because ≈_{E} is by definition preserved under substitution.

We call the pair (Σ, E) a presentation of the algebraic theory � if there is an isomorphism � ≅ Cxt_{Σ}/E. We call it a finite presentation if both Σ and E are finite.

We now conclude our running example of monoid actions.

4.19. Example. In Example 4.4, we gave the signature for monoid actions on sets, with sorts m, s and function symbols η, μ, α. To present the algebraic theory of monoid actions on sets, we add the following four equations:

x : m ⊢ μ(x, η) = x  x, y, z : m ⊢ μ(x, μ(y, z)) = μ(μ(x, y), z)
x : m ⊢ μ(η, x) = x  x : m, y : m, p : s ⊢ α(x, α(y, p)) = α(μ(x, y), p)

4.20. Definition. Define the category of algebraic presentations APr as follows: the objects of APr are pairs (Σ, E), where Σ is an algebraic signature and E is a set of equations over Σ. A morphism F: (Σ, E) → (Σ′, E′) is a morphism F: Σ → Σ′ in the Kleisli category ASig^{∗} such that F (t) ≈_{E′} F (t′) for each equation t = t′ of E.

Let Cxt also denote the functor APr → ATh sending a pair (Σ, E) to Cxt_{Σ}/E.

4.21. Remark. Any algebraic theory � has a canonical presentation (Σ_{�}, E_{�}), where Σ_{�} is the underlying signature from Example 4.5, and E_{�} is defined such that an equation x_{1} : s_{1}, …, x_{n} : s_{n} ⊢ (t = t′) : s is in E_{�} if and only if the morphisms corresponding to t and t′ in the hom-set � (s_{1} × ⋯ × s_{n}, s) are equal.

It is not hard to see that Cxt_{Σ_{�}}/E_{�} ≅ � for any algebraic theory �. It is also straightforward to check that Cxt : APr → ATh is fully faithful, and hence an equivalence of categories.

The following easy proposition establishes the fundamental connection between a presentation for an algebraic theory � and algebras on �.

4.22. Proposition. Let Σ be an algebraic signature and E be a set of equations, and consider an assignment of a set F_{s} to each sort s ∈ S_{Σ} and a function F_{f}: F_{s_{1}}×⋯×F_{s_{n}} → F_{s′} to each function symbol f: (s_{1}, …, s_{n}) → s′ in Φ_{Σ}. This assignment uniquely extends to a Cxt_{Σ}-algebra F. In particular, given any term (x_{1} : s_{1}, …, x_{n} : s_{n}) ⊢ t : s′, there is a function F_{t}: F_{s_{1}} × ⋯ × F_{s_{n}} → F_{s′}.

The assignment uniquely extends to a Cxt_{Σ}/E-algebra if and only if it satisfies the equations E, i.e. for each equation Γ ⊢ t_{1} = t_{2} of E, the functions F_{t_{1}} and F_{t_{2}} are equal.

4.23. Example. Consider the presentation (Σ, E), where S_{Σ} = {Int} is the only sort, Φ_{Σ} consists of the five function symbols 0, 1: () → Int, (−): (Int) → Int, and +, ×: (Int, Int) → Int, and E is the set of equations shown in Fig. 1. The algebraic theory � = Cxt_{Σ}/E generated by this presentation is a category with objects the contexts over Σ, such as

x, y, z : Int ⊢ (x + y) + z = x + (y + z)
x : Int ⊢ x + 0 = x
x, y : Int ⊢ x + y = y + x
x : Int ⊢ x + (−x) = 0
x, y, z : Int ⊢ (x × y) × z = x × (y × z)
x : Int ⊢ x × 1 = x
x, y : Int ⊢ x × y = y × x
x, y, z : Int ⊢ x × (y + z) = (x × y) + (x × z)

Figure 1: Equations for the algebraic theory of commutative rings.

(a : Int) or (x, y, z : Int). Some example context morphisms (x, y, z : Int) → (a : Int) are [a := (x + y) × (x + z)] and [a := ((x × x) + (x × z)) + ((y × x) + (y × z))]. These context morphisms are equivalent under ≈_{E}, so determine the same morphism in �.

It is possible to show that the category �-Alg is equivalent to the category CRing of commutative rings. In particular, a product preserving functor F: � → Set must send the context (a : Int) to some set R, the context morphism [a := x + y]: (x, y : Int) → (a : Int) to a function R × R → R, etc.

We name the single sort ‘Int’ to fit with the practice in type theory, in which the “elements” of a type τ are considered to be the ground terms of type τ. That the ground terms of sort ‘Int’ are precisely the integers is equivalent to the fact that � is the initial commutative ring.

We will use the following algebraic theory throughout the paper in our database examples.

4.24. Example. Consider the multi-sorted algebraic theory Type generated by the finite theory presentation with base sorts, function symbols and equations as defined in Fig. 2, page 573. It may be helpful to recall that implication can be written as (a ⇒ b) = ¬a ∨ b. We use an axiomatization of Boolean algebras which is proven complete in [Hun04].

Clearly this algebraic theory includes the one from Example 4.23 as a sub-theory. Similarly to viewing ground terms of type ‘Int’ as the integers, those of type ‘Str’ are strings of letters, presented as the free monoid on 52 generators (upper and lower case letters). For example, when we later write ‘Admin′ : Str we actually mean the term ∅ ⊢ ‘A′.‘d′.‘m′.‘i′.‘n′ : Str.^{3} It can be shown that the ground terms of type ‘Bool’ are {True, False}.

4.25. Presentations of algebras. We now turn to presentations of algebras. Fix a presentation (Σ, E), and let � = Cxt_{Σ}/E be the presented algebraic theory. Recall by Definition 4.6 how we can think of objects in Set_{/S_{Σ}}, the category of S_{Σ}-indexed sets, as (possibly infinite) contexts over Σ. There is an evident forgetful functor U: �-Alg → Set_{/S_{Σ}}, which sends an algebra A: � → Set to the indexed set {(UA)_{s}}_{s∈S_{Σ}} where (UA)_{s} = A(s).

3Similarly, we may use the shorthand x − y to denote what is really x + (−y).

ALGEBRAIC DATABASES  573

S_{Σ} : Int, Bool, Str
Φ_{Σ} : 0, 1 : () → Int (−) : (Int) → Int +, × : (Int, Int) → Int ≤ : (Int, Int) → Bool ⊤, ⊥ : () → Bool ¬ : (Bool) → Bool ∧ : (Bool, Bool) → Bool ∨ : (Bool, Bool) → Bool ε, ‘a′, …, ‘Z′ : () → Str (.) : (Str, Str) → Str eq : (Str, Str) → Bool

E : boolean algebra:
α : Bool ⊢ α ∨ ⊥ = α  α : Bool ⊢ α ∧ ⊤ = α
α, β : Bool ⊢ α ∨ β = β ∨ α  α, β : Bool ⊢ α ∧ β = β ∧ α
α : Bool ⊢ α ∨ ¬α = ⊤  α : Bool ⊢ α ∧ ¬α = ⊥
α, β, γ : Bool ⊢ α ∨ (β ∧ γ) = (α ∨ β) ∧ (α ∨ γ) α, β, γ : Bool ⊢ α ∧ (β ∨ γ) = (α ∧ β) ∨ (α ∧ γ)

commutative ring: all equations from Fig. 1 totally pre-ordered ring:

x, y, z : Int ⊢ ¬((x ≤ y) ∧ (y ≤ z)) ∨ (x ≤ z) = ⊤
x, y : Int ⊢ (x ≤ y) ∨ (y ≤ x) = ⊤
x, y, z, w : Int ⊢ ¬((x ≤ y) ∧ (z ≤ w)) ∨ (x + z ≤ y + w) = ⊤
x, y, z : Int ⊢ ¬((x ≤ y) ∧ (0 ≤ z)) ∨ (x × z ≤ y × z) = ⊤
x, y, z : Int ⊢ ¬((x × z ≤ y × z) ∧ (0 ≤ z)) ∨ (x ≤ y) = ⊤
∅ ⊢ (1 ≤ 0) = ¬⊤

monoid:

s : Str ⊢ s.ε = s s, t, u : Str ⊢ (s.t).u = s.(t.u)
s : Str ⊢ ε.s = s

congruence:

s : Str ⊢ (s eq s) = ⊤
s, t : Str ⊢ (s eq t) = (t eq s)
s, t, u : Str ⊢ ¬((s eq t) ∧ (t eq u)) ∨ (s eq u) = ⊤
s, t, u, v : Str ⊢ ¬((s eq t) ∧ (u eq v)) ∨ (s.u eq t.v) = ⊤

decidable equality:

s, t, u : Str ⊢ (s.u eq t.u) = (s eq t)
s, t, u : Str ⊢ (s.t eq s.u) = (t eq u)
s, t : Str ⊢ (s.‘a′ eq t.‘b′) = ¬⊤ … s, t : Str ⊢ (s.‘y′ eq t.‘z′) = ¬⊤
s, t : Str ⊢ (‘a′.s eq ‘b′.t) = ¬⊤ … s, t : Str ⊢ (‘y′.s eq ‘z′.t) = ¬⊤
s : Str ⊢ (s.‘a′ eq ϵ) = ¬⊤  …  s : Str ⊢ (s.‘z′ eq ϵ) = ¬⊤
s : Str ⊢ (‘a′.s eq ϵ) = ¬⊤  …  s : Str ⊢ (‘z′.s eq ϵ) = ¬⊤

Figure 2: Presentation of Type, our running example of an algebraic theory.

4.26. Definition. Let Γ ∈ Set_{S_{Σ}} be an S_{Σ}-indexed set, thought of as a context, and let � = Cxt_{Σ}/E be a presented algebraic theory. Define the free �-algebra on Γ, denoted κ[Γ]: � → Set, to be the algebra for which κ[Γ](Θ) is the set of ≈_{E}-equivalence classes of context morphisms Γ → Θ, with functoriality given by composition of context morphisms.

4.27. Remark. With notation as in Definition 4.26, the elements of κ[Γ] of sort s are just the ≈_{E}-equivalence classes of terms Γ ⊢ t : s, and for any function symbol f: (s_{1}, …, s_{n}) → s′ the induced function sends a tuple of terms Γ ⊢ t_{i} : s_{i} to the term Γ ⊢ f(t_{1}, …, t_{n}) : s′. By Proposition 4.22, this completely defines the algebra κ[Γ], whose standard name is the term algebra over Γ. There is an adjunction

κ[–]: Set_{S_{Σ}} ⇆ (Cxt_{Σ}/E)-Alg :U  (22)

For this reason, we may refer to κ[Γ] as the free algebra on the generating context Γ.

4.28. Example. Let � be any algebraic theory. The algebra generated by the empty context is the algebra of constants κ[∅] = κ = y(1); see Example 3.4. Note that any term in κ is necessarily a ground term (Definition 4.8). If X is any other �-algebra, we refer to terms in the image of the unique map κ → X as constants in X.

4.29. Example. Let � be the algebraic theory from Example 4.23. The elements of κ[x, y : Int] of the unique base sort ‘Int’ are ≈_{E}-equivalence classes of terms x, y : Int ⊢ t : Int, such as x, y : Int ⊢ (x + y) × x. But these are just polynomials in the variables x and y, hence the commutative ring κ[x, y : Int] ∈ �-Alg is the polynomial ring �[x, y], the free commutative ring on the set {x, y}.

4.30. Remark. Note that the Kleisli category for the adjunction (22) is precisely the opposite of the category \overline{Cxt_{Σ}}/E of possibly infinite contexts (Definition 4.13), and the restriction of this Kleisli category to those objects X → S_{Σ} of Set_{/S_{Σ}} for which X is finite is the category (Cxt_{Σ}/E)^{op}. Another way to say this is that the algebraic theory Cxt_{Σ}/E is isomorphic to the opposite of the category of finitely generated free algebras over Cxt_{Σ}/E, a fact which is true for any algebraic theory; see [ARV11, § 8].

4.31. Definition. Let Σ be an algebraic signature, Γ a context over Σ, and e an equation over Σ. Say that e is an equation in Γ if it is between terms in context Γ. A set E′ of equations over Σ is said to be in Γ if each element e ∈ E′ is.

4.32. Definition. Let (Σ, E) be a presentation for an algebraic theory �. A �-algebra presentation is a pair (Γ, E′), where Γ is a context over Σ, and E′ is a set of equations in Γ. Define κ[Γ]/E′ to be the quotient of the free �-algebra κ[Γ] (Definition 4.26) by the equations E′. Concretely, (κ[Γ]/E′)(Θ) is the set of ≈_{E∪E′}-equivalence classes of context morphisms Γ → Θ.

A morphism of �-algebra presentations (cf. Definition 4.20) (Γ′, E′) → (Γ′′, E′′) is simply a context morphism [x⃗ := t⃗]: Γ′′ → Γ′ (note the direction!) such that for each equation Γ′ ⊢ u = v in E′, it follows that Γ′′ ⊢ u[x⃗ := t⃗] ≈_{E∪E′′} v[x⃗ := t⃗].

4.33. Example. Let (Σ, E) be the theory of commutative rings as in Example 4.23, and let Γ = (x, y : Int). Then κ[Γ] is the polynomial ring �[x, y] (Example 4.29). If e is the equation x^{3} = y^{2} then (κ[Γ]/{e}) is the ring �[x, y]/(x^{3} − y^{2}).

4.34. Remark. Recall that by Remark 4.21, every algebraic theory has a canonical presentation and the functor APr → ATh from presentations to theories is an equivalence. For algebras the same turns out to be true. First, every �-algebra A ∈ (Cxt_{Σ}/E)-Alg has a canonical presentation (Γ, E′), where Γ is the underlying S_{Σ}-indexed set UA, and E′ is the set of equations Γ ⊢ t = t′ for which t and t′ are equated under the counit κ[Γ] → A of the adjunction from (22). Second, the category of such presentations (whose objects and morphisms are given in Definition 4.32) is equivalent to �-Alg.

4.35. Presentations of categories. It is well known that categories are algebraic over directed graphs, i.e. that a category can be presented by giving a graph together with a set of equations (see e.g. [Mac98, § II.8]). In the interest of completeness and consistency, we will show here how to consider presentations for categories as a special case of presentations for algebraic theories (see Definition 4.41).

Formally, a directed graph G consists of a set G_{0} of nodes and a set G_{1} of edges, together with functions dom, cod: G_{1} → G_{0}. Note that a directed graph G can be seen as an algebraic signature (Definition 4.2) in which all function symbols are unary. The set of sorts of the unary signature is simply the set G_{0} of nodes of G, and the set G_{1} of edges is taken as the set of function symbols.

4.36. Definition. Say that an algebraic signature Σ is unary when all of its function symbols are unary. As usual, we will write f: A → B as shorthand for dom(f) = A and cod(f) = B. From now on, we will identify a graph G with its corresponding unary algebraic signature.

4.37. Remark. Let G be a graph, and let A, B ∈ G_{0} be nodes. Terms (Definition 4.8) of type B in a singleton context (x : A) over (the unary signature associated to) G can be identified with paths from A to B in G. As G has only unary function symbols, all such terms must be of the form x : A ⊢ f_{n}(… f_{2}(f_{1}(x))) : B for some n ≥ 0.

4.38. Proposition. Let G be a graph and Fr(G) the free category generated by G. Then Fr(G) is isomorphic to the full subcategory of Cxt_{G} spanned by the singleton contexts.

4.39. Notation. Let Σ be an algebraic signature, and let Γ ⊢ t be a term in some context. In order to reduce parentheses, we will use the notation Γ ⊢ t.f_{1}.f_{2} … f_{n} to denote Γ ⊢ f_{n}(… f_{2}(f_{1}(t))), assuming that this is a well-formed term and that each f_{i} is unary.

4.40. Definition. Let Σ be a (not necessarily unary) signature. An equation Γ ⊢ t = t′ over Σ is unary if the context Γ is a singleton. Say that a set E of equations is unary if it consists only of unary equations.

4.41. Definition. A category presentation is a pair (G, E), where G is a graph and E is a set of unary equations over G. Define the category presented by (G, E), denoted Fr(G)/E, to be the full subcategory of Cxt_{G}/E spanned by the singleton contexts.

4.42. Proposition. Let (G, E) be a category presentation. The category Cxt_{G}/E is the free category-with-finite-products on the category Fr(G)/E. In particular, there is an equivalence of categories (Cxt_{G}/E)-Alg ≃ [Fr(G)/E, Set].

4.43. Presentations of set-valued functors. If � is a category given by a presentation (G, E), then Proposition 4.42 provides a way of giving presentations for functors � → Set. Let Γ be a context over the unary algebraic signature G. Then we can form the free algebra κ[Γ] ∈ (Cxt_{G}/E)-Alg as in Definition 4.26. Under the equivalence (Cxt_{G}/E)-Alg ≃ [�, Set], this corresponds to a functor � → Set, namely the restriction of κ[Γ]: Cxt_{G}/E → Set to its full subcategory of singleton contexts �. We will denote this restriction ⟨Γ⟩.

It is straightforward to check that the adjunction from Remark 4.27 restricts to an adjunction ⟨–⟩: Set_{G_{0}} ⇆ [�, Set] :U. Hence ⟨Γ⟩ is the free copresheaf on � generated by Γ.

Similarly, if E′ is a set of equations in context Γ, as in Definition 4.31, then we denote by ⟨Γ⟩/E′ the restriction of κ[Γ]/E′: Cxt_{G}/E → Set to �, and refer to this as the copresheaf presented by (Γ, E′).

4.44. Presentations of algebraic profunctors. In Section 5 we will be interested in algebraic profunctors M: � � where � is a category and � is an algebraic theory; see Definition 3.10. Our approach to presenting an algebraic profunctor M between � = Fr(G)/E_{G} and � = Cxt_{Σ}/E_{Σ} will be in terms of its collage M̃, as in Example 2.19.

4.45. Definition. Let G = (G_{0}, G_{1}) be a graph (unary signature) and Σ = (S_{Σ}, Φ_{Σ}) be an algebraic signature. A profunctor signature Υ from G to Σ is a set of unary function symbols, where each function symbol att ∈ Υ is assigned a sort a := dom(att) ∈ G_{0} and a sort τ := cod(att) ∈ S_{Σ}. We will sometimes refer to the function symbol att ∈ Υ as an attribute, and denote it att: a → τ.

A profunctor signature Υ has an associated algebraic signature Υ̃ = (SΥ̃, ΦΥ̃), with sorts SΥ̃ = G_{0} ⊔ S_{Σ}, and function symbols ΦΥ̃ = G_{1} ⊔ Υ ⊔ Φ_{Σ}.

Say that a set E_{Υ} of equations over Υ̃ is a set of profunctor equations if for each equation Γ ⊢ (t_{1} = t_{1}) : s′ in E_{Υ}, the context is a singleton Γ = (x : s) with s ∈ G_{0} and s′ ∈ S_{Σ}.

4.46. Definition. Let (G, E_{G}) be a category presentation, (Σ, E_{Σ}) an algebraic theory presentation, Υ a profunctor signature from G to Σ, and E_{Υ} a set of profunctor equations. Let EΥ̃ = E_{G} ∪ E_{Σ} ∪ E_{Υ}. Define the algebraic profunctor presented by this data, denoted κ[Υ]/E_{Υ} : Fr(G)/E_{G} Cxt_{Σ}/E_{Σ}, as follows:

• for any node a ∈ G_{0} and context Γ ∈ Cxt_{Σ}, the set (κ[Υ]/E_{Υ})(a, Γ) is the hom set (CxtΥ̃/EΥ̃)((x : a), Γ), i.e. the set of ≈_{E_{G}∪E_{Σ}∪E_{Υ}}-equivalence classes of context morphisms (x : a) → Γ over Υ̃, • the functorial actions are given by substitution.

It is clear from the definition that the collage of the profunctor κ[Υ]/E_{Υ} is a full subcategory of CxtΥ̃/EΥ̃. In fact, it is not much harder to see the following proposition; cf. Proposition 4.42.

4.47. Proposition. Let � be a category with presentation (G, E_{G}), let � be an algebraic theory with presentation (Σ, E_{Σ}), and let P: � � be an algebraic profunctor with presentation (Υ, E_{Υ}). The category CxtΥ̃/EΥ̃ is the free completion of the collage P̃ under finite products for which existing products in � are preserved. In particular, the category (CxtΥ̃/EΥ̃)-Alg of functors (CxtΥ̃/EΥ̃) → Set which preserve all finite products is equivalent to the category of functors P̃ → Set whose restriction to � preserves finite products.

4.48. Example. Let � be the category presented by the terminal graph G_{0} = {X}, G_{1} = {f}, with equation x : X ⊢ x.f = x.f.f. Let � be the algebraic theory of commutative rings, as in Example 4.23. Consider the algebraic profunctor M: � � presented by a single attribute Υ = {p: X → Int} and a single equation E = {x : X ⊢ x.f.p = x.p×x.p}. One can check that this presents the following profunctor � �:

κ[Υ]/E_{Υ} ≅ �[x.f^{n}.p]/( x.f^{n+1}.p = (x.f^{n}.p)^{2} , x.f^{n+2}.p = x.f^{n+1}.p )
≅ �[y_{0}, y_{1}]/( y_{1} = y_{0}^{2} , y_{1} = y_{1}^{2} )
≅ �[y]/( y^{2} = y^{4} )

where, in the first line, n ranges over all natural numbers. The edge f ∈ G_{1} induces the ring endomorphism f(y) ↦ y^{2}.

5. Algebraic database schemas

In this section we move beyond background and into our construction of databases. What we call (algebraic) databases straddle what are traditionally known as relational databases and the more modern graph databases. Importantly, algebraic databases also integrate a programming language Type, by which to operate on attribute values.

We take our terminology from the relational database world. That is, a database consists of a conceptual layout, called a schema, as well as some conforming data, called an instance (because it represents our knowledge in the current instant of time). In this section we discuss the category of schemas; in Section 6 we discuss instances on them.

5.1. Schemas. For the rest of the paper, Type will be an arbitrary multi-sorted finitely presented algebraic theory, as defined in Definition 4.18. However, in all examples, we will fix Type to be the algebraic theory described in Example 4.24. Recall from Definition 3.10 the notion of algebraic profunctors M ∈ Prof^{×}(�, Type), denoted M: � Type.

5.2. Definition. A database schema S over Type is a pair (S_{e}, S_{o}), where • S_{e} is a category, and

• S_{o} : S_{e} Type is an algebraic profunctor; i.e. S_{o} ∈ Prof^{×}(S_{e}, Type). We refer to S_{e} as the entity category of S and to S_{o} as the observables profunctor. We will also write S_{o} : S_{e}^{op} → Type-Alg for the exponential transpose of S_{o} : S_{e}^{op} × Type → Set; see Lemma 3.9.

5.3. Remark. It is often convenient to work with schemas in terms of their collages. If S is the schema S_{o} : S_{e} Type, we write S̃ for the collage of the profunctor S_{o}; see Example 2.19. By (13), it comes equipped with a map S̃ → 2 and we refer to the two pullbacks below respectively as the entity side and the type side of the collage:

\begin{matrix}S_{e} & S̃ & Type \\ \{∗\} & 2 & \{∗\} \end{matrix} i_{S} ! ⌟ i_{T} ! ⌞ 0 1

5.4. Example. Any Type-algebra X: Type → Set can be regarded as a schema ({∗}, X), where the entity category is terminal. In particular, the initial Type-algebra κ, described in Example 3.4, can be viewed as a schema U = ({∗}, κ) called the unit schema.^{4}

5.5. Presentations of schemas. A presentation for a schema S_{o} : S_{e} Type is simply a presentation for the category S_{e} (see Definition 4.41) together with a presentation for the algebraic profunctor S_{o} (see Definition 4.46). We spell this out in Definition 5.6.

5.6. Definition. A schema signature Ξ = (G_{Ξ}, Υ_{Ξ}) consists of a graph G_{Ξ} together with a profunctor signature Υ_{Ξ} from G_{Ξ} to the signature of Type.

A schema presentation (Ξ, E_{Ξ}) consists of a schema signature Ξ, together with equations E_{Ξ} = (E_{e}, E_{o}), where E_{e} is a set of unary equations over G_{Ξ}, and E_{o} is a set of profunctor equations over Υ_{Ξ}. Note that (G_{Ξ}, E_{e}) is a presentation for a category, which will be the entity category S_{e}, and (Υ_{Ξ}, E_{o}) is a presentation for an algebraic profunctor S_{e} Type. We denote the presented schema by Fr(Ξ)/E_{Ξ}.

We will write Ξ̃ to mean the associated algebraic signature Υ̃_{Ξ} as in Definition 4.45, with sorts (G_{Ξ})_{0} ⊔ S_{Σ} and function symbols (G_{Ξ})_{1} ⊔ Υ_{Ξ} ⊔ Φ_{Σ}, where Type ≅ Cxt_{Σ}/E_{Σ}.

In what follows, we refer to function symbols in Υ_{Ξ} as attributes, and refer to a general term (x : A) ⊢ t : τ, where A ∈ (G_{Ξ})_{0} and τ ∈ Type, as an observable on A of type τ. In other words, for a schema S_{o} : S_{e} Type and objects A ∈ S_{e} and τ ∈ Type, an observable on A of type τ is an element t ∈ S_{o}(A, τ).

5.7. Example. The unit U = ({∗}, κ) of Example 5.4 is presented by the graph with one vertex and no edges, the empty profunctor signature, and no equations. That is, U has no attributes, so each of its observables is a ground term ∅ ⊢ c : τ, i.e. a constant c ∈ κ(τ) = Type(1, τ).

4U is the unit of a certain symmetric monoidal structure on Schema (Definition 5.11), whose restriction to entities is the cartesian monoidal structure on Cat; however, we do not pursue that here.

Entities: Emp, Dept

Edges:

               mgr : Emp → Emp
               wrk : Emp → Dept
               sec : Dept → Emp

Path Eqs:

               e : Emp ⊢ e.mgr.mgr = e.mgr
               e : Emp ⊢ e.mgr.wrk = e.wrk
               d : Dept ⊢ d.sec.wrk = d

Attributes:

                                                    last : Emp → Str
                                                    name : Dept → Str
                                                    sal : Emp → Int

Obs. Eqs: e : Emp ⊢

(e.sal ≤ e.mgr.sal) = ⊤

Figure 3: Presentation of S, our running example of a schema.

5.8. Example. Let Type be as in Example 4.24. Consider the presentation (Ξ, E_{e}, E_{o}) for a schema S as displayed in Fig. 3, which will serve as a motivating example throughout the paper. In this presentation, we use the labels "Entities" for (G_{Ξ})_{0}, "Edges" for (G_{Ξ})_{1}, "Attributes" for Υ_{Ξ}, "Path Eqs" for E_{e}, and "Obs. Eqs" for E_{o}.

Below (23) is a graphical display of this presentation; its two grey dots are the entities, its six arrows are the edges and attributes, and its four equations are the path and observable equations.

                        Dept Emp Int Str Bool wrk mgr sal last sec name^{mgr.mgr = mgr mgr.wrk = wrk sec.wrk = id (sal ≤ mgr.sal) = ⊤} S  (23)

The presented schema S is built according to Definitions 4.41 and 4.46, as we now describe explicitly. The entity category S_{e} is the free category on the subgraph of grey objects and arrows between them, modulo the top three equations. An example (context) morphism Emp → Dept in S_{e} is given by the path mgr.wrk.sec.mgr.wrk. From the equations, we can show that it is equivalent to wrk,

                e : Emp ⊢ (e.mgr.wrk.sec.mgr.wrk ≈ e.wrk) : Dept

In other words, these two terms name the same morphism in S_{e}.

The observables profunctor S_{o} : S_{e} Type is freely generated by the three arrows from an S_{e}-object to a Type-object , modulo the fourth equation. An example observable Dept → Bool, i.e. an element of S_{o}(Dept, Bool), is "whether a department d is named Admin", given by the term (d : Dept) ⊢ eq(d.name, Admin). By the fourth equation, we can show it is equivalent to a more complex observable,

d : Dept ⊢ ((d.sec.sal ≤ d.sec.mgr.sal) ∧ eq(d.name, Admin)) : Bool.

The schema S can accommodate database instances in some company setting, as we will see in Example 6.3. In such, there exist tables of employees and departments. In each there are columns (sometimes called foreign keys) that reference other tables in order to state where an employee works, who is the departmental secretary, etc. There are also columns that state the last name and salary of each employee, etc. The equations express integrity constraints, e.g. the fact that the secretary of a department works therein, or that every employee is paid less than his or her manager.

5.9. Schema mappings. We now discuss morphisms of schemas, also known as schema mappings [DHI12]. These will eventually be the vertical morphisms in a proarrow equipment. Recall by Definition 3.10 that a morphism between two algebraic profunctors is just a 2-cell between profunctors as in (9).

5.10. Definition. A schema mapping F: S → T is a pair (F_{e}, F_{o}), where • F_{e} : S_{e} → T_{e} is a functor, and

• F_{o} is a 2-cell in �rof

S_{e}  Type

T_{e}  Type

S_{o}

F_{e}

T_{o}

⇓F_{o}

We will also write F_{o} for the corresponding natural transformation F_{o} : S_{o} ⇒ T_{o} ∘ F_{e}^{op} of functors S_{e}^{op} → Type-Alg.

5.11. Definition. Define the category of schemas, denoted Schema, to have database schemas as objects and schema mappings as morphisms.

5.12. Remark. From the universal property of collages (Definition 2.16) in �rof, it follows easily that a schema mapping F: S → T is equivalently a functor F̃ over 2 between their collages, as in the left-hand diagram

\begin{aligned}S̃ & & T̃ \\ & 2 \end{aligned} F̃ p p′  \begin{matrix}S_{e} & T_{e} \\ S̃ & T̃ \end{matrix} F_{e} i_{S} i_{T} F̃  Type  Type S̃  T̃ i_{T} i_{T} F̃ (24)

such that the middle and right-hand diagrams are the pullbacks of the left-hand diagram along the two maps 1 → 2; see (13) and Remark 5.3. By definition, a schema mapping acts as identity on the Type-side of the collages.

5.13. Example. Consider the schema presentation given by the following graph, attributes, and equations:

                          Dept QR Emp Int Str Bool f g wrk mgr sal last sec name^{mgr.mgr = mgr mgr.wrk = wrk sec.wrk = id (sal ≤ mgr.sal) = ⊤ (f.sal ≤ g.sec.sal) = ⊤ f.wrk.name = Admin} T  (25)

The schema T which it presents, includes S of Example 5.8. In addition it has a new entity QR — named for its eventual role as a query result table in Section 9 — as well as two new edges f, g, and two new observable equations

q : QR ⊢ (q.f.sal ≤ q.g.sec.sal) = ⊤, q : QR ⊢ q.f.wrk.name = Admin.  (26)

Thus we have a schema inclusion G: S → T, which of course restricts to identity on the Type-side by definition.

5.14. Example. We will now describe another schema mapping, with codomain the above schema T. We will again do so in terms of presentations:

           A Int Str Bool diff emp_last dept_name QR Dept Emp Int Str Bool f g wrk mgr sal last name sec plus eqs from (25) T R F

The schema R has a terminal entity category R_{e} = {A}, along with three generating attributes — namely diff, emp_last, and dept_name — from the unique object to the base Type-sorts Str, Int. Schema T has six equations, whereas R has none.

The schema mapping F: R → T viewed as a functor F̃: R̃ → T̃, is defined to map the unique object A ∈ R_{e} to QR ∈ T_{e} on the entity side, and to map the three attributes to the following observables in T:

    diff ↦ g.sec.sal − f.sal    emp_last ↦ f.last    dept_name ↦ g.name

Since on the type side it is identity and R has no equations, there is nothing more to check; we have defined a schema mapping. This choice will be justified by Remark 9.6.

              Emp    last   wrk  mgr  sal

e1 Gauss d3 e1 250
e2 Noether d2 e4 200
e3 Einstein d1 e3 300
e4 Turing d2 e4 400
e5 Newton d3 e1 100
e6 Euclid d2 e7 150
e7 Hypatia d2 e7 x

                                                Dept   name   sec

d1  HR  e3
d2 Admin e6
d3  IT  e5

Figure 4: Example of an S-instance J.

6. Algebraic database instances

6.1. Instances and transforms. Given a database schema S, which is a conceptual layout of entities and their attributes (see Definition 5.2), we are ready to assign each entity a table full of data laid out according to the schema. Such an assignment is called an instance on S; it is a set-valued functor (copresheaf) of a certain form. Morphisms between instances are often called (attribute-preserving) database homomorphisms [AHV95], but we call them transforms because they are nothing more than natural transformations.

6.2. Definition. Let S be a database schema, S̃ its collage, and i_{T} : Type → S̃ the inclusion of the type side (see Remark 5.3). An S-instance I is a functor I: S̃ → Set such that the restriction I_{t} := I ∘ i_{T} preserves finite products, i.e. I_{t} : Type → Set is a Type-algebra.

Define the category of S-instances, denoted S-Inst, to be the full subcategory of the functor category [S̃, Set] spanned by the S-instances. A morphism α: I → J of instances is called a transform.

6.3. Example. Recall the schema S generated by the presentation of Example 5.8, which had employees and departments as entities, edges and attributes such as manager and salary, and equations such as an employee’s salary must be less than that of his or her manager. A summary of an S-instance J is displayed in Fig. 4, with one table for each entity in S, and with a column for each edge and attribute.

All data required to determine an instance is encapsulated in the above two tables (image of the entity side and the attributes) along with a choice of Type-algebra, which is generally infinite. Here, the Type-algebra must include not only constants, but also all terms using the indeterminate x : Int, which expresses Hypatia’s unknown salary. Moreover, the equation e : Emp ⊢ (e.sal ≤ e.mgr.sal) = ⊤ in the presentation of S implies that the terms 150 ≤ x and ⊤ must be equal in J(Bool) (by letting e = e6 ).

Explicitly, we can define the functor J: S̃ → Set as follows: the restriction J_{t} = J ∘i_{T} to Type is the presented type algebra

J_{t} ≅ κ[x : Int]/(150 ≤ x = ⊤),

and J is defined on entities by the following sets:

J(Emp) = {e1 , e2 , e3 , e4 , e5 , e6 , e7 }, J(Dept) = {d1 , d2 , d3 },

and on edges and attributes by functions as shown in the table, e.g.

J(wrk): J(Emp) → J(Dept) by e1 ↦ d3 , …, e7 ↦ d2
J(name): J(Dept) → J(Str)  by d1 ↦ HR, …, d3 ↦ IT

6.4. Example. Let S be as in Example 5.8. Consider another S-instance J̄, which is the same as J except that e7 is removed from J̄(Emp) and the restriction J̄_{t} = J̄∘ i_{T} to Type is just κ, the algebra of constants as in Example 3.4. We will have use for both J and J̄ later.

6.5. Definition. We refer to instances whose Type-algebra is initial, i.e. I_{t} = κ, as ground instances. So J from Example 6.3 is not a ground instance but J̄ from Example 6.4 is. If a Type-algebra is presented by generators and relations, generators (such as the indeterminate value ‘x’ of Example 6.3) are often referred to as labelled nulls or Skolem variables [AHV95].

Even though it wasn’t defined that way, the category of instances S-Inst can be seen to be the category of algebras for an algebraic theory. Proving this, as we do next, immediately gives us several nice properties of the category S-Inst.

6.6. Proposition. For any schema S, the category of instances S-Inst is equivalent to the category of algebras for an algebraic theory.

Proof. Recall from Definition 3.3 the category of algebras for a theory. We can consider S̃ as a finite-product sketch, whose designated product cones are all finite products in Type. Then a model of this sketch is a functor S̃ → Set which preserves finite products in Type, i.e. an instance of S. The category of models for any finite product sketch is equivalent to the category of algebras for an algebraic theory generated by the sketch; see e.g. [BW85, §4.3].

6.7. Remark. When given a presentation (Ξ, E_{Ξ}) for a schema S, as in Definition 5.6, we can make Proposition 6.6 much more concrete: combining Proposition 4.47 and Definition 6.2, it follows that there is an equivalence of categories S-Inst ≃ (CxtΞ̃/EΞ̃)-Alg.

6.8. Corollary. For any schema S, the category of instances S-Inst has all small colimits.

Proof. This follows from 6.6 and 3.5.

6.9. Remark. As in Warning 3.6, we note that colimits in S-Inst do not always agree with the pointwise colimits in [S̃, Set], which can make them difficult to work with. However, the following simple observation is sometimes useful:

Let X: � → S-Inst be a diagram and let U(X) be its composite with the inclusion S-Inst → [S̃, Set]. If the colimit colim(UX) in [S̃, Set] lands in the subcategory S-Inst (i.e. preserves products in Type), then the natural map colim(UX) → U(colim X) is an isomorphism. In other words, in this case, the colimit colim X can be taken pointwise. (Note that this observation only uses the fact that S-Inst is a full subcategory of [S̃, Set]).

6.10. Example. Let ∅ ∈ Schema be the initial schema, i.e. the unique schema having an empty entity category. Then ˜∅ ≅ Type, thus there is an isomorphism of categories

∅-Inst ≅ Type-Alg.

6.11. Remark. Notice that for any schema S, the Yoneda embedding y: S̃^{op} → [S̃, Set] is product-preserving and hence factors through the forgetful functor S-Inst → [S̃, Set]. The left factor S̃^{op} → S-Inst, which we also denote y, is fully faithful. In particular, for any object s ∈ S̃, the representable functor y(s): S̃ → Set given by y(s)(x) = S̃(s, x) is an instance, called the S-instance represented by s.

Because the functor S-Inst → [S̃, Set] is fully faithful, it follows that the embedding y: S̃^{op} → S-Inst is dense (see Remark 3.7). In particular, for any instance I ∈ S-Inst, there is a canonical isomorphism of S-instances

I ≅ ∫ ^{s∈S̃} I(s) · y(s)

which also follows from Remark 6.9.

6.12. Presentations of instances. Let (Ξ, E_{Ξ}) be a presentation of a schema S (Definition 5.6) and Ξ̃ its associated algebraic signature, whose generated theory is the free product completion of its collage S̃ (Proposition 4.47). By Remark 6.7, we can use presentations of algebras for a theory (Definition 4.32) to give presentations of S-instances.

6.13. Definition. Let Γ be a context over the above algebraic signature Ξ̃. The free (CxtΞ̃/EΞ̃)-algebra κ[Γ] corresponds under the equivalence of Proposition 6.6 to an Sinstance, which we denote ⟨Γ⟩, and call the free S-instance generated by Γ.

If E_{Γ} is a set of equations in context Γ, then we similarly write ⟨Γ⟩/E_{Γ} for the Sinstance corresponding to κ[Γ]/E_{Γ}, and call it the S-instance presented by (Γ, E_{Γ}). Concretely, (⟨Γ⟩/E_{Γ}) (s) = {terms in context Γ of type s ∈ S̃}/∼, by Remark 4.27.

6.14. Example. For any object s ∈ S̃, the representable instance y(s) as in Remark 6.11 is free, with one generator of type s, i.e. y(s) ≅ ⟨(x : s)⟩.

            Emp           last           wrk         mgr         sal
             e  e.last  e.wrk  e.mgr  e.sal
           e.mgr  e.mgr.last  e.wrk  e.mgr  e.mgr.sal
           d.sec  d.sec.last  d.sec.wrk = d d.sec.mgr  d.sec.sal
         d.sec.mgr  d.sec.mgr.last  d  d.sec.mgr d.sec.mgr.sal
          e.wrk.sec  e.wrk.sec.last  e.wrk  . . .  . . .

e.wrk.sec.mgr  …  …  …  …

                             Dept   name     sec
                              d  d.name  d.sec

e.wrk Admin e.wrk.sec

Figure 5: Example of a presented S-instance I.

6.15. Remark. Similar to Remark 4.34, any given instance I has a canonical presentation, where for each s ∈ S̃ and x ∈ I(s) there is a generator x : s, and for each arrow f: s → s′ in S̃ with y = I(f)(x), there is an equation x : s ⊢ x.f = y. In this way, the presentation essentially records every entry of every column in every table.

For example, the canonical presentation of J from Example 6.3 has context and equations

Γ = (e1 , …, e7 : Emp, d1 , d2 , d3 : Dept, x : Int)
E = {e1 .last = Gauss, e1 .wrk = d3 , …, d3 .sec = e5 }

(27)

6.16. Example. Let S be as in Example 5.8. We will now describe an S-instance I that is fairly different-looking than that in Example 6.3 or 6.4, in that the values of most of its attributes are non-constants. Instances like I play a central role in database queries (see Section 9).

We specify the instance I by means of a presentation I = ⟨Γ⟩/E_{Γ}, where Γ = (e : Emp, d : Dept), and where E_{Γ} contains the two equations

Γ ⊢ e.wrk.name = Admin
Γ ⊢ (e.sal ≤ d.sec.sal) = ⊤.

(28)

Thus for any entity or type s ∈ S̃, the elements of I(s) are the equivalence classes of terms Γ ⊢ t : s built out of edges and attributes from S and function symbols from Type, modulo the equations E_{Γ} as well as those from S.

We can picture this instance in the tables shown in Fig. 5. On types, I contains many terms, as in

I(Str) = {e.last, e.mgr.last, d.sec.last, …, d.name, Admin, …, aaBcZ, … }
I(Int) = {e.sal, e.mgr.sal, …, −d.sec.sal, e.sal + e.sal + 1, …, 28734, … }
I(Bool) = {eq(e.last, d.name), …, e.mgr.sal ≤ d.sec.sal, …, ⊤, ¬⊤}

Note, for example, that the value of e.wrk.name in the table Dept has been replaced by ‘Admin’ because of an equation of I and that the value of e.wrk.sec.wrk has been replaced by e.wrk because of a path equation of S (see Example 5.8).

6.17. Example. Having defined two S-instances J and I in the examples 6.3 and 6.16 above, we will now explicitly describe the set S-Inst(I, J) of instance transforms between them.

By Remarks 4.34 and 6.7, the set of transforms I → J is equivalent to the set of morphisms of presentations from the presentation (Γ, E_{Γ}) of I to the canonical presentation of J. Such a morphism of presentations is simply an assignment of an element ϵ ∈ J(Emp) to the generator e : Emp and an element δ ∈ J(Dept) to the generator d : Dept, such that the two equations ϵ.wrk.name = Admin and (ϵ.sal ≤ δ.sec.sal) = ⊤ are true in J.

Without the equations, there would be 21 assignments (ϵ, δ) ∈ J(Emp) × J(Dept). It is easy to check that only three of those 21 satisfy the two equations: (e6 , d1 ), (e2 , d1 ), and (e6 , d2 ). For instance, the equation e.wrk.name = Admin means we must have ϵ.wrk = d2 . Similarly, the equation ((e.sal) ≤ d.sec.sal) = ⊤ rules out several choices. For example, the assignment (ϵ, δ) := (e7 , d1 ) is invalid because we cannot deduce that x ≤ 300 from any equations of J (where we only know that 150 ≤ x).

6.18. Example. We will now consider transforms between two instances that are both presented. As usual, let S be the schema of Example 5.8, and let I be the instance from above, Example 6.16. We recall its presentation (Γ_{I}, E_{I}), as well as present a new S-instance I′:

Γ_{I′} = {e′ : Emp}  Γ_{I} = {e : Emp, d : Dept}
E_{I′} = {e′.wrk.name = Admin (e′.sal ≤ e′.wrk.sec.sal) = ⊤}  E_{I} = {e.wrk.name = Admin (e.sal ≤ d.sec.sal) = ⊤}

As in Definition 4.32, to give an instance transform β: I′ ⇒ I, it is equivalent to give a context morphism Γ_{I} → Γ_{I′} (see Definition 4.11) in the opposite direction which respects the equations. In this case, there are only two which satisfy the equations: [e′ := e] and [e′ := e.wrk.sec].

6.19. Decomposing instances. While Definition 6.2 is how we most often consider instances, it will sometimes be useful to consider their entity and attribute parts separately. Recall the left action ⊗ of Definition 3.11 on algebraic profunctors.

An instance I on a schema S is equivalently defined to be a tuple (I_{e}, I_{t}, I_{o}), where • I_{e} : {∗} S_{e} is a profunctor, called the entity side of I,

• I_{t} : {∗} Type is an algebraic profunctor, called the type side of I, and

• I_{o} : I_{e} ⊗ S_{o} → I_{t} is a profunctor morphism, called the values assignment for I:

\begin{aligned}& S_{e} \\ \{∗\} & & Type \end{aligned} S_{o} I_{e} I_{t} ⇓I_{o}

The functor I: S̃ → Set of Definition 6.2, viewed as I: {∗} S̃, can then be uniquely recovered by the lax limit universal property of S̃ spelled out in Remark 2.32, for X = {∗}.

Note that the entity side I_{e} : S_{e} → Set is just a copresheaf, the type side I_{t} : Type → Set is just a Type-algebra, and the values assignment I_{o} is equivalent to a morphism ∫^{s∈S_{e}} I_{e}(s) · S_{o}(s) → I_{t} of Type-algebras (where the coend is in Type-Alg, see Theorem 3.5). We could also obtain I: S̃ → Set from collages universal property (11) in �rof.

Similarly, a transform I → J between instances can equivalently be defined in terms of separate entity and type components (α_{e}, α_{t}), where α_{e} : I_{e} ⇒ J_{e} and α_{t} : I_{t} ⇒ J_{t} are profunctor morphisms, satisfying the equation:

\{∗\}  S_{e}  Type I_{e} J_{e} J_{t} S_{o} ⇓α_{e} ⇓J_{o} =  \begin{aligned}& S_{e} \\ \{∗\} & & Type \end{aligned} S_{o} I_{e} I_{t} J_{t} ⇓I_{o} ⇓α_{t}

Given α: I ⇒ J: S̃ → Set, the entity and type components α_{e} and α_{t} are simply the restrictions of α along the collage inclusions i_{S}: S_{e} → S̃ ← Type :i_{T}. In the other direction, given α_{e} and α_{t}, one recovers α by the 2-dimensional part of the universal property of Remark 2.32.

7. The fundamental data migration functors

In this section, we describe functors that transfer instances from one schema to another. More specifically, we show how any schema mapping F: S → T induces a system of three adjoint functors

T-Inst  S-Inst

Δ_{F}

Π_{F} ⊥

Σ_{F} ⊥

which we call data migration functors. They are related to the usual Kan extensions setting between categories of presheaves. Recall from Definition 5.10 that a schema mapping F: S → T is a functor F_{e} : S_{e} → T_{e} and a 2-cell F_{o}:

S_{e}  Type

T_{e}  Type

S_{o}

F_{e}

T_{o}

⇓F_{o}

7.1. Definition. Let F: S → T be a schema mapping, and let F̃: S̃ → T̃ be the induced map on collages (Remark 5.12). We define a functor Δ_{F} : T-Inst → S-Inst as follows:

• For any instance I of T, define Δ_{F} (I) := I ∘ F̃. By (24) and Definition 6.2, the following diagram commutes:

\begin{aligned}& Type \\ S̃ & T̃ & Set \end{aligned} i_{T} i_{T} I_{t} F̃ I

Thus Δ_{F} (I)_{t} = I ∘ F̃ ∘ i_{T} = I_{t} preserves products.

• For any α: I → J in T-Inst, define Δ_{F} (α) = α ∘ F̃. We call Δ_{F} the pullback functor (along F).

7.2. Example. For any schema S, the unique map !: ∅ → S from the initial schema (Example 6.10) induces a functor Δ_{!} : S-Inst → Type-Alg, denoted Δ_{!_{S}}. For an instance I of S, this functor returns the underlying Type-algebra of the instance, Δ_{!_{S}}(I) ≅ I_{t}.

A schema mapping F can be considered as a map of finite product sketches; see Proposition 6.6. In general one does not expect the pullback functor Δ_{F} between the corresponding categories of algebras to have a right adjoint; for example, there is no ‘cofree monoid’ on a set. However, because F restricts to the identity on the Type-side of the collage by Remark 5.12, we find that Δ_{F} does have a right adjoint, denoted Π_{F}, which we call the right pushforward functor.

7.3. Proposition. Let F: S → T be a schema mapping. The right Kan extension RanF̃: [S̃, Set] → [T̃, Set] takes S-instances to T-instances, defining a right adjoint to Δ_{F},

Δ_{F} : T-Inst ⇆ S-Inst :Π_{F}

Proof. Let I: S̃ → Set be any functor. Then for an object x ∈ T̃, the right Kan extension is given by

Π_{F} (I)(x) := (RanF̃I)(x) ≅ [T̃, Set] (T̃(x, −), RanF̃(I))
≅ [S̃, Set] (T̃(x, F̃−), I)
≅ ∫_{s∈S̃} I(s)^{T̃(x,F̃s)}.

(29)

We will show that this formula preserves the property of I_{t} being product-preserving. In fact, it preserves the Type-algebra exactly, i.e. the diagram on the left commutes (up to natural isomorphism)

[S̃, Set]  [T̃, Set]

[Type, Set]

RanF̃

–∘i_{T}

–∘i_{T}

Type  Type

S̃  T̃. id i_{T} i_{T} F̃ (30)

or equivalently, the pullback square on the right satisfies the Beck-Chevalley condition for right Kan extensions. The latter follows formally because the inclusion i_{T} : Type → T̃ is an opfibration, but we can easily check the commutativity of the left diagram directly: for any τ ∈ Type, (29) gives

(RanF̃I)(τ) ≅ [S̃, Set] (T̃(τ, F̃–), I) ≅ [S̃, Set] (S̃(τ, –), I) ≅ I(τ),

completing the proof.

We now define the left pushforward functor, denoted Σ_{F}.

7.4. Proposition. For any schema mapping F: S → T, the functor Δ_{F} has a left adjoint

Σ_{F} : S-Inst ⇆ T-Inst :Δ_{F} .

If I ∈ S-Inst is an instance, then Σ_{F} (I) is given by the following coend taken in T-Inst:

Σ_{F} (I) ≅ ∫ ^{s∈S̃} I(s) · y(F̃s),  (31)

where y(F̃s) is the representable T-instance T̃(F̃s, −), see Remark 6.11.

In other words, Σ_{F} is the left Kan extension

S̃^{op}  T̃^{op} S-Inst  T-Inst F̃^{op} y y Σ_{F} =Lan_{y}(y∘F̃)  (32)

and the above square in fact commutes.

Proof. The coend exists because T-Inst is cocomplete (Corollary 6.8). It is simple to check that this defines a left adjoint to Δ_{F}:

T-Inst (∫ ^{s∈S̃} I(s) · y(F̃^{op}(s)), J) ≅ ∫_{s∈S̃} T-Inst(I(s) · y(F̃^{op}(s)), J)
≅ ∫_{s∈S̃} Set(I(s), T-Inst(y(F̃^{op}(s)), J))
≅ ∫_{s∈S̃} Set(I(s), J(F̃(s)))
≅ [S̃, Set] (I, J ∘ F̃) = S-Inst(I, Δ_{F} (J)).

The square commutes since Σ_{F} : S-Inst → T-Inst is a pointwise Kan extension along the fully faithful y.

7.5. Remark. The coend (31) is not typically a pointwise colimit, as pointed out in Remark 6.9. Hence, unlike Π or Δ, given an object t ∈ T̃ there is in general no explicit formula for computing the set (Σ_{F} (I))(t).

However, obtaining the presentation of Σ(I) from a presentation of I is almost trivial: if I is presented by a context Γ = (x_{1} : s_{1}, ..., x_{n} : s_{n}) and some equations, then Σ_{F} (I) is presented by the context F (Γ) = (x_{1} : F̃(s_{1}), ..., x_{n} : F̃(s_{n})) and respective equations by applying F̃ to edges, attributes of the term expressions.

7.6. Remark. For any schema mapping F: S → T, one can check using (30) and Definition 7.1 that the functors Π_{F} and Δ_{F} preserve Type-algebras, in the sense that (Π_{F} I)_{t} ≅ I_{t} and (Δ_{F} J)_{t} ≅ J_{t}. This does not generally hold for Σ; in Proposition 7.12 we give a simple criterion for when it does.

7.7. Example. We will give an example of the application of the left pushforward functor Σ_{H}: S-Inst → L-Inst on J from Example 6.3, for a schema mapping H: S → L as follows:

                Dept

                Emp

Int Str Bool

                     wrk mgr sal last name sec

                Team

                Dept

                Emp

Int Str Bool

                     on wrk mgr sal last bel col sec name

                     mgr.on = on
                     on.bel = wrk

plus eqs from (23) plus eqs from (23)

L S

H

Schema S is as in Example 5.8, and schema L has a new entity ‘Team’, thought of as grouping employees into teams, which have a color-name and belong to some department. The two new equations ensure that an employee is on the same team as their manager and that their team belongs to their department.

The functor H̃: S̃ → L̃ is an inclusion, preserving labels (H̃(Emp) = Emp, etc.). Thus, by Remark 7.5, we find that the presentation of Σ_{H}(J) is exactly that of J, shown in (27), only now interpreted as a L-instance presentation. To calculate the L-instance it presents, one follows the explanation from Section 6.12 (as we explain briefly below) and finds that Σ_{H}(J) is given by the tables shown in Fig. 6, where t1 , t2 , t3 , t4 are freely generated terms. The Type-algebra of this instance is larger than that of I; it includes, for example, new terms t1 .col, …, t4 .col : Str.

To calculate the set of rows in the Team table, following Definition 6.13 one freely adds a new team for each employee to be on, but quotients by setting each employees team equal to that of his or her manager, due to the equation (mgr.on = on) : Team in schema L. Notice how we have one team belonging to HR and one team belonging to IT, but two teams belonging to Admin. This basically results from the freeness of the construction and the fact that there are two different managers, Turing and Hypatia, in

   Team   col   bel

t1 t1 .col d3
t2 t2 .col d2
t3 t3 .col d1
t4 t4 .col d2

                        Emp    last   wrk  mgr  sal  on

e1 Gauss d3 e1 250 t1
e2 Noether d2 e4 200 t2
e3 Einstein d1 e3 300 t3
e4 Turing d2 e4 400 t2
e5 Newton d3 e1 100 t1
e6 Euclid d2 e7 150 t4
e7 Hypatia d2 e7 x t4

                                                           Dept   name   sec

d1  HR  e3
d2 Admin e6
d3  IT  e5

Figure 6: The left pushforward instance, Σ_{H}(J) ∈ L-Inst.

Admin. The colors assigned to these teams are freely assigned as indeterminate string values (e.g. t1 .col) in those cells.

7.8. Example. Recall the schema mapping G: S → T from Example 5.13, which is given by the inclusion of the S-presentation (23) into the T-presentation (25). We are going to describe the effect of the induced right pushforward functor Π_{G}: S-Inst → T-Inst on the S-instance J of Example 6.3.

The T-instance Π_{G}(J): T̃ → Set is given by an ordinary right Kan extension, as expressed by formula (29). Its Type-algebra coincides with that of J, namely it is the presented algebra κ[x : Int]/∼. Because G is of a particularly simple form, the only thing that remains to compute is Π_{G}(J)(QR), which is the following subset of J(Emp) × J(Dept):

                                   QR   f   g

qr1 e2 d1
qr2 e6 d1
qr3 e6 d2

These three elements of the product are the ones that satisfy the supplementary equations of the presentation of T (i.e. f.sal≤g.sec.sal=⊤ and f.wrk.name=Admin). Its columns Π_{G}(J)(f) and Π_{G}(J)(g) represent the respective projections to Π_{G}(J)(Emp) = J(Emp) and Π_{G}(J)(Dept) = J(Dept). As usual, the names qr1 , qr2 , and qr3 are not canonical; perhaps more canonical names would be (e2 , d1 ), (e6 , d1 ), and (e6 , d2 ).

7.9. Remark. One may notice that there is an isomorphism between the set Π_{G}(J)(QR) from Example 7.8 and the set S-Inst(I, J) from Example 6.17. The reason is that there is in fact an isomorphism of S-instances T̃(QR, G̃−) ≅ I, as is most evident by observing the similarity between the defining equations (26) and (28).

7.10. Example. Recall the schema mapping F: R → T described in Example 5.14. Here we will discuss the pullback Δ_{F} (K), where K := Π_{G}(J) is computed in Example 7.8. Briefly, the table presentation of K consists of the tables Emp, Dept as in Example 6.3 and QR as in 7.8, and its Type-algebra is κ[x : Int]/∼.

The R-instance Δ_{F} (K): R̃ → Set is obtained by pre-composing with F̃, as in Definition 7.1. It has the same Type-algebra (Remark 7.6), and its one entity table is

                        A   emp_last  dept_name  diff

qr1 Noether  HR  100
qr2 Euclid  HR  150
qr3 Euclid  Admin  0

We conclude this section with some special cases for which Σ is nicely behaved.

7.11. A pointwise formula for Σ. Given an arbitrary mapping F: S → T and Sinstance I, the formula for the functor Σ_{F} (I): T̃ → Set cannot be given pointwise on objects t ∈ T̃. However, there is a special kind of schema mapping F for which we can write a pointwise formula for Σ_{F} (I), namely those which induce a discrete opfibration on collages F̃: S̃ → T̃. This occurs if and only if F̃ arises via the Grothendieck construction applied to a functor ∂F: T̃ → Set, for which the composite ∂F ∘ i_{T} : Type → T̃ → Set is terminal. Note that in this case, we have a bijection

Ob S̃ ≅ { (t, p) | t ∈ T̃, p ∈ ∂F (t) } ≅ ∐_{t∈T̃} ∂F (t).

One can show using ends, the adjunction Σ ⊣ Δ, and the fact that S-Inst ⊆ [S̃, Set] is fully faithful, that Σ_{F} is then given by the following pointwise formula:

Σ_{F} (I)(t) = ∐_{p∈∂F (t)}I(t, p).

In particular, Σ_{F} preserves Type-algebras in this case, i.e. Σ_{F} (I)(τ) = I(τ) for any τ ∈ Type.

It is easy to show that if F̃ is a discrete opfibration, then F_{o} is cartesian, so the preservation of Type-algebras can also be seen as a special case of the following result.

7.12. Proposition. The left pushforward Σ_{F} along a schema mapping F = (F_{e}, F_{o}): S → T preserves type-algebras if and only if F_{o} is cartesian.

Proof sketch. Consider the commutative square in Schema shown here:

\begin{aligned}& ∅ \\ R & & S \end{aligned} ; !_{R} ; !_{S} ; F

By Example 7.2 it suffices to show that F_{o} is cartesian if and only if the restriction of the unit map Δ_{!_{R}}η: Δ_{!_{R}} → Δ_{!_{R}}Δ_{F} Σ_{F} = Δ_{!_{S}}Σ_{F} coming from Σ_{F} ⊣ Δ_{F} is an isomorphism. Both sides preserve colimits, so since y is dense, Δ_{!_{R}}η is an isomorphism if and only if the components Δ_{!_{R}}(η_{y(r)}) are isomorphisms for any r ∈ R̃. For τ ∈ Type, η_{y(τ)} is always an isomorphism. For r ∈ R̃, we have Δ_{!_{R}}(y(r)) = R_{o}(r) and Δ_{!_{S}}Σ_{F} (y(r)) = S_{o}(F_{e}(r)) by (32). It is not difficult to verify that Δ_{!_{R}}(η_{y(r)}): Δ_{!_{R}}(y(r)) → Δ_{!_{S}}Σ_{F} (y(r)) and the component R_{o}(r) → S_{o}(F_{e}(r)) of F_{o} at r agree, completing the proof.

8. The double category �ata

In this section, we will introduce the notion of a bimodule between two schemas. We will see that bimodules generalize instances on a schema, as well as queries, which are the subject of Section 9. We will show that schemas, schema mappings, and bimodules together form an equipment, which we denote �ata. For database-style examples of material from this section, see Section 9.

8.1. Relevant terminology and notation. Recall that companions and conjoints in �rof are given by representable profunctors, as explained in Example 2.12. Also recall from Definition 3.10 that a profunctor M whose codomain is an algebraic theory � is called algebraic if it is product-preserving on the right; it is denoted M: � � . If S is a schema, then the functor i_{T} : Type → S̃ denotes the inclusion of Type into the collage (Remark 5.3).

8.2. Bimodules between schemas. Bimodules admit several equivalent definitions, and it is convenient to be able to switch between these definitions as best suits the task at hand. We will begin with the one which we use most often.

8.3. Definition. Let R and S be database schemas. A bimodule M: R S is a functor M: R̃^{op} → S-Inst such that the following diagram commutes:

Type^{op}  S̃^{op}

R̃^{op}  S-Inst

i_{T}^{op} i_{T}^{op} y M

(33)

or succinctly, M(τ) = y(τ) for any τ ∈ Type.

A morphism of (R, S)-bimodules ϕ: M → N is a natural transformation ϕ: M ⇒ N that restricts to the identity on Type. We denote by _{R}Bimod_{S} the category of (R, S)- bimodules.

8.4. Remark. It is possible to give Definition 8.3 in a more symmetric form. A bimodule M: R S is equivalently a profunctor M̃: R̃ S̃ between collages such that:

• the composite profunctor R̃ M̃ S̃ î_{T} Type is algebraic, and

• the composite profunctor Type î_{T} R̃ M̃ S̃ is isomorphic to the representable î_{T} : Type S̃.

A morphism of (R, S)-bimodules ϕ: M → N is equivalently a profunctor transformation ϕ̃: M̃ ⇒ Ñ such that î_{T} ⊙ ϕ̃ = idî_{T}.

While this formulation of bimodules may be useful for intuition, we will primarily use Definition 8.3 in this paper.

8.5. Adjoints Λ and Γ. Considering a bimodule M: R S as a functor R̃^{op} → S-Inst, we can apply the left Kan extension along the Yoneda embedding R̃^{op} → R-Inst; see Remark 6.11. The result is denoted Λ_{M} := Lan_{Y} (M),

R̃^{op}  S-Inst

M R-Inst y Λ_{M} (34)

Since S-Inst is cocomplete (Corollary 6.8), we can express this using the Kan extension formula (cf. (2))

\begin{aligned}Λ_{M}(I) & = ∫ ^{r∈R̃} R-Inst(y(r), I) · M(r) \\ & ≅ ∫ ^{r∈R̃} I(r) · M(r) \end{aligned}  (35)

where · is the Set-theoretic copower on S-Inst. Because the Yoneda embedding is fully faithful, it follows that this Kan extension really is an extension, i.e. (34) commutes. It also follows that Λ_{M} “preserves types,” that is, that the following diagram commutes:

Type^{op}

R-Inst  S-Inst

y y Λ_{M}

(36)

A bimodule M: R S also determines a functor in the other direction,

Γ_{M}: S-Inst  R-Inst
J  S-Inst(M(–), J). (37)

The condition (33) on M implies that for any object τ ∈ Type,

(Γ_{M}J)(τ) = S-Inst(M(τ), J) = S-Inst(y(τ), J) = J(τ)  (38)

from which it easily follows that Γ_{M}(J) preserves products of types, hence defines an object in R-Inst. We thus say that Γ “preserves type-algebras”, in the sense that the following diagram commutes:

S-Inst  R-Inst

Type-Alg

Γ_{M}

U

U

8.6. Proposition. For any bimodule M: R S, the functor Λ_{M} is left adjoint to Γ_{M}.

Proof. This is simply a calculation:

S-Inst(Λ_{M}I, J) = S-Inst (∫ ^{r∈R̃} I(r) · M(r), J)
≅ ∫_{r∈R̃} S-Inst(I(r) · M(r), J)
≅ ∫_{r∈R̃} Set(I(r), S-Inst(M(r), J))
= ∫_{r∈R̃} Set(I(r), (Γ_{M}J)(r)) ≅ R-Inst(I, Γ_{M}J).

The first isomorphism follows because homs take colimits in their first variable to limits, while the second is the definition of copower.

8.7. Lemma. We collect here several easy but useful properties of Λ:

1. For any schema S, there is an isomorphism of functors Λ_{y} ≅ id_{S-Inst}.

2. For any bimodule M: R̃^{op} → S-Inst and any left adjoint L: S-Inst → T-Inst, there is an isomorphism of functors Λ_{L∘M} ≅ L ∘ Λ_{M}. In particular,

3. For any bimodules M: R S and N: S T, there is an isomorphism of functors Λ_{Λ_{N} ∘M} ≅ Λ_{N} ∘ Λ_{M}.

Proof. Property 1 is simply the fact that y is dense (see Remark 6.11), while property 2 is the fact that left adjoints preserve colimits, hence preserve pointwise left Kan extensions. Finally, property 3 follows from property 2 using Proposition 8.6.

8.8. Remark. The Λ_{M} ⊣ Γ_{M} adjunction is an instance of the general geometric realization/nerve adjunction Set^{�^{op}} ⇆ � induced by a functor F: � → � into a cocomplete category � (see e.g. [Lei04, pp. 244–245] or [nLab]). In this case, F is the functor M: R̃^{op} → S-Inst. The conditions in Definition 8.3 guarantee that the nerve functor lands in the full subcategory R-Inst ⊆ [R̃, Set].

8.9. Equivalent definitions of bimodules. In Theorem 8.10 we give five equivalent definitions of bimodules, and we will give a few others throughout the section, e.g. in Propositions 8.20 and 8.24 and Corollary 8.35. The ones we discuss here are aligned with the analogy presented in Section 2.2, by which profunctors between categories and linear transformations between vector spaces can be related. The only complication here is that all of our structures must deal carefully with the algebraic theory Type, as we now make explicit.

Consider the coslice 2-category Type^{op}/𝒞at. An object is a pair (�, F), where � ∈ 𝒞at is a category and F: Type^{op} → � is a functor; a morphism (�, F) → (�, G) is a functor H: � → � such that H ∘ F = G; and a 2-cell H → H′, where H, H′: (�, F) → (�, G), is a natural transformation α: H ⇒ H′ such that αF = id_{G}.

For any schema S, both S-Inst and S̃^{op} can be considered objects in Type^{op}/𝒞at (via y and i_{T}^{op}). Similarly, S-Inst can be considered an object in the slice 2-category 𝒞at/Type-Alg, where the functor S-Inst → Type-Alg simply sends an instance S̃ → Set to its restriction along the inclusion i_{T} : Type → S̃.

8.10. Theorem. Let R and S be schemas. The following are equivalent:

1. The category _{R}Bimod_{S} of bimodules R S.

2. The category (Type^{op}/𝒞at)(R̃^{op}, S-Inst).

3. The category of profunctors R̃ S̃ satisfying the conditions of Remark 8.4.

4. The category ℒ Adj_{Type}(R-Inst, S-Inst), which we define to be the full subcategory of (Type^{op}/𝒞at)(R-Inst, S-Inst) spanned by left adjoint functors.

5. The category ℛ Adj_{Type}(S-Inst, R-Inst)^{op}, whose opposite is defined to be the full subcategory of (𝒞at/Type-Alg)(S-Inst, R-Inst) spanned by right adjoint functors.

Proof. 1 and 2 are equivalent by Definition 8.3, and it is easy to check the equivalence between 1 and 3.

For the equivalence of 2 and 4, consider the functor

(– ∘ y): ℒ Adj_{Type}(R-Inst, S-Inst) → (Type^{op}/Cat)(R̃^{op}, S-Inst).

Its inverse is Λ_{−}, the left Kan extension along y: R̃^{op} → R-Inst, which lands in ℒ Adj_{Type}(R-Inst, S-Inst) by (36) and Proposition 8.6. To see that these are inverses, note that by commutative (34) we have Λ_{M}(y(r)) = M(r). For the other direction, we have by Lemma 8.7

Λ_{L∘y} ≅ L ∘ Λ_{y} ≅ L ∘ id_{S-Inst} = L.

Finally, we show that 4 and 5 are equivalent. The equivalence ℒ Adj(R-Inst, S-Inst) ≃ ℛ Adj(S-Inst, R-Inst)^{op} is standard, so we only need to show that this equivalence respects the restrictions concerning Type. In one direction, if L: R-Inst → S-Inst is a left adjoint satisfying (36), then we check that the right adjoint G of L satisfies (38):

(GJ)(τ) ≅ R-Inst(y(τ), GJ)
≅ S-Inst(L(y(τ)), J)
≅ S-Inst(y(τ), J)
≅ J(τ).

Conversely, if G: S-Inst → R-Inst is a right adjoint satisfying (38), then

S-Inst(L(y(τ)), J) ≅ R-Inst(y(τ), RJ)
≅ (GJ)(τ)
≅ J(τ)
≅ S-Inst(y(τ), J),

hence by the Yoneda lemma, L(y(τ)) ≅ y(τ), for any τ ∈ Type.

8.11. Proposition. For any schemas R and S, the category _{R}Bimod_{S} has finite colimits.

Proof. The initial object of _{R}Bimod_{S} is given by the left Kan extension of the Yoneda embedding Type^{op} → S-Inst along the collage inclusion Type^{op} → R̃^{op}. Concretely, the initial bimodule 0 can be described by cases:

0(r, s) = \begin{cases}R̃(r, s) & if s is a type \\ ∅ & otherwise. \end{cases}

To complete the proof, we need to show that _{R}Bimod_{S} has pushouts. By Theorem 8.10, RBimod_{S} ≃ (Type^{op}/𝒞at)(R̃^{op}, S-Inst), and by Corollary 6.8, S-Inst is cocomplete. Let us fix a choice of pushouts in S-Inst, such that the chosen pushout of the constant span on an instance I is I. Then it is easy to check that _{R}Bimod_{S} is closed under the induced chosen pointwise pushouts in 𝒞at(R̃^{op}, S-Inst), and that these are in fact pushouts in the subcategory (Type^{op}/𝒞at)(R̃^{op}, S-Inst).

8.12. The equipment �ata. We are now ready to assemble schemas, schema morphisms, and bimodules into a single double category �ata, which we define in Definition 8.13, and which we show to be an equipment in Proposition 8.14. In order to define the double category structure, we will need the easy notion of restriction of bimodules along schema morphisms.

Suppose we have a bimodule N: R′ S′, and schema mappings F: R → R′ and G: S → S′. Thinking of N as a functor N: R̃^{′op} → S′-Inst as in Definition 8.3, we can form the bottom composite

R̃^{op}  S-Inst

(R̃′)^{op}  S′-Inst

F̃^{op}

F N_{G}

N

Δ_{G}

and define a bimodule _{F}N_{G} : R S so that the square commutes. This construction defines a functor _{F} Bimod_{G}: _{R′}Bimod_{S′} → _{R}Bimod_{S}. By computing the composite Δ_{F} ∘ N ∘ F̃^{op} on objects, it easily follows that (_{F} N_{G}(r))(s) = Ñ(F̃r, G̃s) for any r ∈ R̃ and s ∈ S̃, where N is viewed as Ñ: R̃′ S̃′. This is relevant to Remark 8.15.

8.13. Definition. We define the double category �ata as follows: the objects of �ata are schemas, the vertical morphisms are schema mappings, and the horizontal morphisms are bimodules. We define a 2-cell of the form

\begin{matrix}R & S \\ R′ & S′ \end{matrix}

M F G N ⇓θ

(39) to be a natural transformation θ: M → Δ_{G} ∘ N ∘ F̃^{op}:

R̃^{op}  S-Inst

R̃′^{op}  S′-Inst,

M

F̃^{op}
N

Δ_{G}

⇓θ

i.e. a morphism θ ∈ _{R}Bimod_{S}(M,_{F}N_{G}). Equivalently, it is a 2-cell θ̃: M̃ ⇒ Ñ in �rof with frames L(θ̃) = F̃ and R(θ̃) = G̃, and which has identity components on r ∈ Type.

Given bimodules M: R S and N: S T, we define their composite M ⊙ N by

M ⊙ N := Λ_{N} ∘ M: R̃^{op} → S-Inst → T-Inst.  (40)

where Λ_{N} is as defined in (35). The unit bimodule U_{R} : R R for any schema R is given by the Yoneda embedding y: R̃^{op} → R-Inst, since Λ_{M} ∘ y ≅ M by (34). It corresponds to the unit in �rof, Ũ_{R} := UR̃ : R̃ R̃.

The horizontal composition of 2-cells

\begin{matrix}R & S & T \\ R′ & S′ & T′ \end{matrix} M F N G H M′ N′ ⇓θ ⇓ϕ  (41)

is defined by the composition

R̃^{op}  S-Inst  T-Inst

R̃′^{op}  S′-Inst  S′-Inst  T′-Inst

M

F̃^{op}
Σ_{G}

Λ_{N}

M′

Δ_{G}

Λ_{N′}

Δ_{H}

⇓θ

⇓

⇓Λ_{ϕ}

where the middle triangle is the counit of the Σ_{G} ⊣ Δ_{G} adjunction. Vertical composition of 2-cells works in the evident way.

The data above satisfy the axioms of a double category as in Definition 2.8, with vertical category �ata_{0} = Schema and horizontal ℋ (�ata)(R, S) = _{R}Bimod_{S}.

8.14. Proposition. The double category �ata is an equipment.

Proof. It is clear from the definition of 2-cells in �ata that given a niche

\begin{matrix}R & S \\ R′ & S′ \end{matrix} F G N

there is a cartesian filler with the bimodule _{F}N_{G} from Section 8.12 on top.

8.15. Remark. We deduce that the companion and conjoint of a schema mapping F: R → S are the bimodules given by the following formulas:

F̂ = y ∘ F̃^{op} : R̃^{op} → S̃^{op} → S-Inst
F̂ = Δ_{F} ∘ y : S̃^{op} → S-Inst → R-Inst

(42)

These bimodules turn out to be equivalent, via Theorem 8.10, to the companion and conjoint of the induced F̃: R̃ → S̃ in the equipment �rof (3). Moreover, due to Remark 6.9, F̂ ⊙ N ⊙ Ĝ in �ata coincides with ˆ F̃ ⊙ Ñ ⊙ ˇ G̃ in �rof, even though the horizontal compositions differ. This will be put into a larger context in Remark 8.32.

Recall from (37) the definition of Γ, which is right adjoint to Λ by Proposition 8.6.

8.16. Proposition. The equipment �ata is right closed, with N ▷ P := Γ_{N} ∘ P.

Proof. Let M: R S, N: S T and P: R T. By Definition 2.9, it is enough to establish a natural bijection _{R}Bimod_{T}(M ⊙ N, P) ≅ _{R}Bimod_{S}(M, N ▷ P). This follows directly from the Λ_{N} ⊣ Γ_{N} adjunction:

RBimod_{T}(M ⊙ N, P) = T-InstR̃^{op}(Λ_{N} ∘ M, P)
≅ S-InstR̃^{op}(M, Γ_{N} ∘ P)
= _{R}Bimod_{S}(M, N ▷ P),

completing the proof.

In the following, ℒ Adj_{Type} ⊆ Type^{op}/𝒞at and ℛ Adj_{Type} ⊆ 𝒞at/Type-Alg are the obvious sub-2-categories of the (co)slices described in Section 8.9.

8.17. Proposition. There is a commutative diagram of pseudofunctors and bicategories, each of which is a local equivalence:

ℒ Adj_{Type} ; ℋ (�ata) ; ℛ Adj_{Type}^{op}

≃

Λ_{−}

Γ_{−}

Proof. On objects, Λ_{–} maps a schema S to the functor y: Type^{op} → S-Inst; on bimodules and 2-cells, it is was described in Theorem 8.10. Then for any bimodules M: R S and N: S T, we have Λ_{M⊙N} := Λ_{Λ_{N} ∘M} ≅ Λ_{N} ∘ Λ_{M} and Λ_{U_{S}} := Λ_{y} ≅ id_{S-Inst} by Lemma 8.7.

By checking that the coherence axioms are satisfied, this establishes that Λ_{−} is a pseudofunctor. The result follows easily from there.

The following lemma establishes a certain relationship between Λ, Γ and the data migration functors of Section 7. Recall that every schema mapping F: S → T induces a triple adjunction as on the left below, and that every bimodule M: S T induces an adjunction as on the right:

T-Inst  S-Inst

Δ_{F}

Π_{F} ⊥

Σ_{F} ⊥

T-Inst  S-Inst

Γ_{M}

⊥

Λ_{M}

Recall also that every schema mapping F: S → T induces a pair of bimodules F̂: S T and F̂: T S.

8.18. Lemma. For any schema mapping F, we have the following isomorphisms and adjunctions:

(Σ_{F} ≅ ΛF̂) ⊣ (Δ_{F} ≅ ΛF̂ ≅ ΓF̂) ⊣ (Π_{F} ≅ ΓF̂)

Proof. The adjunctions are given in Propositions 7.3 and 7.4, so we provide the isomorphisms. The companion and conjoint of schema mappings are given in (42).

For F: S → T and an instance I ∈ S-Inst, we have an isomorphism

ΛF̂(I) = ∫ ^{s∈S̃} I(s) · F̂(s) ≅ ∫ ^{s∈S̃} I(s) · T̃(F̃s, −) ≅ Σ_{F} (I)

by (35), Remark 8.15 and (31). For any s ∈ S̃ we also have an isomorphism

ΓF̂I(s) = S-Inst(F̂(s), I) ≅ S-Inst(Δ_{F} (ys), I) ≅ Π_{F} I(s)

by (37), Remark 8.15, and Proposition 7.3. The remaining isomorphisms (for Δ) follow by Proposition 8.6.

8.19. Decomposing bimodules. Let M: R S be a bimodule. Since �rof has extensive collages by Example 2.27, the respective profunctor M̃: R̃ S̃ determines an (R_{o}, S_{o})-simplex in the sense of Definition 2.21: four profunctors M_{ee} : R_{e} S_{e}, M_{et} : R_{e} Type, M_{te} : Type S_{e}, and M_{tt} : Type Type, obtained via the restriction of M along the obvious inclusions, together with four 2-cells M_{e∗}, M_{t∗}, M_{∗e}, and M_{∗t}.

The conditions of Remark 8.4 force M_{te} to be the initial profunctor (i.e. the constant functor Type^{op} × S_{e} → Set with value the empty set), M_{tt} to be the unit profunctor (i.e. the hom functor Type^{op} × Type → Set) and M_{et} to be algebraic. Because M_{te} is initial, and because tensor product of profunctors preserves colimits, the 2-cells M_{t∗} and M_{∗e} are unique, and hence don’t need to be specified. Thus we have proven the following proposition, in which we let M_{e} := M_{ee}, M_{t} := M_{et}, M_{o} := M_{e∗}, and M_{r} := M_{∗t}.^{5} 8.20. Proposition. A bimodule M: R S is equivalent to a tuple (M_{e}, M_{t}, M_{o}, M_{r}), where M_{e} : R_{e} S_{e} is a profunctor, M_{t} : R_{e} Type is an algebraic profunctor, and M_{o} and M_{r} are profunctor morphisms

5 The mnemonic for M_{r} comes from its role as "return clause" in queries; see Section 9.4.

\begin{aligned}& S_{e} \\ R_{e} & & Type \end{aligned}

S_{o}

M_{e}

M_{t}

R_{o}

⇓M_{o}

⇑M_{r}

(43)

8.21. Example. For any schema R, the unit bimodule U_{R} : R R is given by

\begin{aligned}& R_{e} \\ R_{e} & & Type \end{aligned}

R_{o} R_{e} R_{o} R_{o} id id

(44)

and the companion/conjoint of a schema mapping F = (F_{e}, F_{o}): R → S decompose as

\begin{aligned}& S_{e} \\ R_{e} & & Type \end{aligned} S_{o} F̂_{e} F̂_{e}⊙S_{o} R_{o} ⇓id ⇑F̂_{o}  \begin{aligned}& R_{e} \\ S_{e} & & Type \end{aligned} R_{o} F̂_{e} S_{o} S_{o} ⇓F̂_{o} ⇑id

where 2-cells F̂_{o}, F̂_{o} are as in Section 2.11 for �rof. This is ‘component-wise’ Remark 8.15.

The equivalence_{F} Res_{G} (Section 2.22) for the extensive collages equipment �rof, which on objects resulted in Proposition 8.20, also gives an equivalent expression of a 2-cell θ

in �ata, viewed as M → ˆ F̃ ⊙ N ⊙ ˆ G̃ inside ℋ (�rof)(S̃, R̃) (see Remark 8.15).

8.22. Proposition. A 2-cell θ in �ata (39) is equivalently a pair of profunctor morphisms

\begin{matrix}R_{e} & S_{e} \\ R′_{e} & S′_{e} \end{matrix} M_{e} F_{e} G_{e} M′_{e} ⇓θ_{e}  R_{e}  Type R′_{e}  Type M_{t} F_{e} M′_{t} ⇓θ_{t}

satisfying the equations

R_{e}  S_{e}  Type R′_{e}  S′_{e}  Type M_{e} F_{e} S_{o} G_{e} M′_{e} M′_{t} S′_{o} ⇓θ_{e} ⇓G_{o} ⇓M′_{o}  =  ^{S_{e} R_{e}  Type R′_{e}  Type S_{o} M_{e} M_{t} F_{e} M′_{t} ⇓M_{o} ⇓θ_{t}}

R_{e}  Type

R′_{e}  Type

R_{o}

M_{t}

F_{e}

M′_{t}

⇓M_{r}

⇓θ_{t}

=  R_{e}  Type R′_{e}  Type R_{o} F_{e} R′_{o} M′_{t} ⇓F_{o} ⇓M′_{r}

(45)

8.23. Corollary. A 2-cell θ in �ata is cartesian if and only if the 2-cells θ_{e} and θ_{t} from Proposition 8.22 are cartesian in �rof.

Because it will be convenient later, we now present yet another equivalent representation of bimodules, which is in some sense intermediate between Definition 8.3 and the completely decomposed representation of Proposition 8.20. Recall from Example 7.2 that for any S-instance I, the underlying Type-algebra is given by I_{t} = Δ_{!_{S}}(I), where !_{S}: ∅ → S is the unique map.

8.24. Proposition. A bimodule M: R S is equivalent to a functor M_{o} : R_{e}^{op} → S-Inst together with a natural transformation

R_{e}^{op}  Type-Alg
R_{o} S-Inst

M_{o}

Δ_{!S}

⇓M_{r}

Proof. The functor M^{op} : R̃ → S-Inst^{op}, opposite to the one given in Definition 8.3, can equivalently be defined — using the universal property (11) of collages in �rof — as a functor M_{o}^{op} : R_{e} → S-Inst^{op}, along with a natural transformation

R_{e}  Type

S-Inst^{op}  S-Inst^{op}.

R_{o} M_{o}^{op} y^{op} S-Inst^{op}

⇓M_{r}

since by definition, types are mapped to representables. This natural family of functions R_{o}(r, τ) → S-Inst (y(τ), M_{o}(r)) equivalently define M_{r} as a natural transformation R_{o} ⇒ Δ_{!_{S}} ∘ M_{o} by Yoneda: S-Inst(y(τ), M_{o}(r)) ≅ M_{o}(r)(τ).

8.25. Instances in terms of bimodules. The category of instances on a schema S can be viewed entirely in terms of bimodules. Indeed, if U = ({∗}, κ) is the unit schema from Example 5.4, then we have an isomorphism of categories

ℋ (�ata)(U, S) ≅ S-Inst.

This follows by comparing their decomposed forms — see Section 6.19 and Propositions 8.20 and 8.22 — and using the fact that κ: {∗} Type is the initial Type-algebra.

It also follows that Λ_{N}(–) is simply given by bimodule composition. Indeed, by (40), for any bimodule N: S T and S-instance J, considered as a (U, S)-bimodule, one has

Λ_{N}(J) ≅ J ⊙ N.  (46)

Similarly, for any T-instance I,

Γ_{N}(I) ≅ J ▷ N.

8.26. Data migration functors in terms of bimodules. We can also recover the fundamental data migration functors from the structure of �ata, using Lemma 8.18 and (46). That is, if we consider instances as bimodules I: U R and J: U S, then composing and exponentiating them with companions and conjoints of F: R → S is equivalent to applying Σ, Δ, Π:

Σ_{F} (I) ≅ I ⊙ F̂,  Δ_{F} (J) ≅ J ⊙ F̂ ≅ F̂ ▷ J,  Π_{F} (I) ≅ F̂ ▷ I

8.27. Collages in �ata. We now consider collages (see Definition 2.16) in the proarrow equipment �ata. Using Proposition 8.20 and the fact that �rof has extensive collages (Example 2.27), we can fully express a collage in �ata in terms of profunctor collages.

Let M = (M_{e}, M_{t}, M_{o}, M_{r}): R S be a bimodule as in (43). Its collage will be a schema Col(M), together with two schema mappings R → Col(M) ← S and a universal 2-cell μ: M ⇒ U_{Col(M)} in �ata. We begin by describing Col(M).

8.28. The schema of a bimodule collage. The entity category of the collage Col(M) is the collage of the profunctor M_{e} : R_{e} S_{e}

Col(M)_{e} := M̃_{e},

and the observables profunctor Col(M)_{o} : M̃_{e} Type is the one uniquely corresponding, via the universal property of the lax colimit M̃_{e} (dual of Remark 2.32), to the cocone

\begin{aligned}S_{e} \\ & Type \\ R_{e} \end{aligned}

S_{o}

M_{e}

M_{t}

⇓M_{o}

In simple words, the functor Col(M)_{o} : M̃_{e}^{op} × Type → Set is given by M_{t} on the R_{e}- side of M̃_{e}, by S_{o} on the S_{e}-side of M̃_{e}, and by M_{o} on the morphisms in between. The profunctor Col(M)_{o} is algebraic, because M_{t} and S_{o} are.

8.29. The schema mappings of a bimodule collage. We now define the collage inclusions i_{R} : R → Col(M) ← S :i_{S}. They are schema mappings as in Definition 5.10, thus each consists of a functor between entity categories and a 2-cell in �rof. The functors between entity categories are the collage inclusions from �rof (see Example 2.19):

(i_{R})_{e} := i_{R_{e}} : R_{e} → M̃_{e} and (i_{S})_{e} := i_{S_{e}} : S_{e} → M̃_{e}.

The 2-cells (i_{R})_{o} and (i_{S})_{o} in �rof are defined respectively as follows:

R_{e}  Type

M̃_{e}  Type

R_{o}

M_{t}

i_{Re}

Col(M)_{o}

⇓M_{r}

⇓cart

and

S_{e}  Type

M̃_{e}  Type

S_{o}

i_{Se}

Col(M)_{o}

⇓cart (47)

The fact that the indicated 2-cells are cartesian follows by definition of Col(M) as a lax colimit; see Proposition 2.30.

8.30. The 2-cell of a bimodule collage. We now define the 2-cell μ in �ata

R  S

Col(M)  Col(M)

M i_{R} i_{S} Col(M)

⇓μ

(48)

in its decomposed form (see Proposition 8.22) to be the pair μ = (μ_{e}, μ_{t})

\begin{matrix}R_{e} & S_{e} \\ M̃_{e} & M̃_{e} \end{matrix} M_{e} i_{Re} i_{Se} M̃_{e} ⇓μ_{e}

R_{e}  Type

M̃_{e}  Type

M_{t}

i_{Re}

Col(M)_{o}

⇓μ_{t}

where μ_{e} is the universal 2-cell for M̃_{e} in �rof (see Example 2.19) and μ_{t} is the (cartesian) square shown to the left in (47). The components μ_{e} and μ_{t} satisfy the equations (45) by the unit bimodule decomposition (44) and the universal property of lax colimit (20).

8.31. Proposition. The equipment �ata has normal collages.

Note that �ata does not have extensive collages. In particular, i_{R} is not in general fully faithful.

Proof. We must first verify that �ata has collages, i.e. that the 2-cell μ defined in (48) has the required universal property (11). Suppose that X is a schema and that ϕ: M ⇒ U_{X} is a 2-cell from M to the unit bimodule. We must show that ϕ factors uniquely through μ:

R  S X  X M F G X ⇓ϕ =  R  S Col(M)  Col(M) X  X M i_{R} i_{S} Col(M) ϕ̄ ϕ̄ X ⇓μ ⇓ϕ̄

We work with components, writing ϕ = (ϕ_{e}, ϕ_{t}) as in Proposition 8.22. Firstly, since μ_{e} is the universal 2-cell for a collage in �rof, we have that ϕ_{e} = Uϕ̄_{e} ∘ μ_{e} for a unique functor ϕ̄_{e} : M̃_{e} → X_{e}. Also, ϕ_{t} = ϕ̄_{t} ∘ μ_{t} as in

R_{e}  Type X_{e}  Type M_{t} F_{e} X_{o} ⇓ϕ_{t} =  R_{e}  Type M̃_{e}  Type X_{e}  Type M_{t} i_{Re} Col(M)_{o} ϕ̄_{e} X_{o} ⇓μ_{t} ⇓ϕ̄_{t}

for a unique 2-cell ϕ̄_{t}, obtained via the 2-dimensional universal property of the lax colimit M̃_{e} (Proposition 2.30). This profunctor morphism ϕ̄_{t} : Col(M)_{o} ⇒ ˆ ϕ̄_{e} ⊙ X_{o} is concretely defined, omitting the details, by natural components

(ϕ̄_{t})_{rτ} = Col(M)_{o}(r, τ) \underrightarrow{∼} M_{t}(r, τ) ⟶^{(ϕ_{t})_{rτ}} X_{o}(F_{e}r, τ) = X_{o}(ϕ̄_{e}r, τ)
(ϕ̄_{t})_{sτ} = Col(M)_{o}(s, τ) \underrightarrow{∼} S_{o}(s, τ) ⟶^{(G_{o})_{sτ}} X_{o}(G_{e}s, τ) = X_{o}(ϕ̄_{e}s, τ)

for r ∈ R_{e}, s ∈ S_{e} and τ ∈ Type. Defining ϕ̄ to be the pair (Uϕ̄_{e}, ϕ̄_{t}): Col(M) → X, we have ϕ = Uϕ̄ ∘ μ as desired.

Moreover, collages in �ata are normal, as in Definition 2.18, since the 2-cell μ constructed in Section 8.30 is cartesian: by Corollary 8.23, it is enough that μ_{e} and μ_{t} are cartesian liftings in �rof.

8.32. Remark. Although we will not use this fact, we note that the collage correspondences from Remarks 5.3, 5.12 and 8.4 provide a lax double functor (see e.g. [GP04])

˜(−): �ata → �rof.

This functor is only lax, because for bimodules R ^{M} S ^{N} T in �ata, the natural map M̃ ⊙ Ñ → { \atop M ⊙ N} in �rof given by the unique transformation in [T̃, Set]

∫ ^{s∈S̃} M̃(r, s) × Ñ(s, −) ⇒ ∫ ^{s∈S̃} M(r)(s) · N(s)

between the pointwise colimit (4) and the T-Inst-one (40), is not an isomorphism (Remark 6.9). Since lax double functors between equipments automatically preserve cartesian liftings (see [Shu08, Prop. 6.4]), this fact also explains Remark 8.15.

8.33. Bimodules in terms of data migration. We will now see that any bimodule, considered as an adjoint functor on instance categories via Theorem 8.10, is equivalent to a composite of data migration functors.

8.34. Corollary. Let M: R S be a bimodule, and let i_{R} : R → Col(M) and i_{S} : S → Col(M) be the collage inclusions. We have isomorphisms

Λ_{M} ≅ Δ_{i_{S}} ∘ Σ_{i_{R}} and Γ_{M} ≅ Δ_{i_{R}} ∘ Π_{i_{S}}

Proof. Since �ata has normal collages, (48) is a cartesian 2-cell, hence M ≅ î_{R} ⊙ U_{Col(M)} ⊙ î_{S}. Therefore, by Lemma 8.18 and Proposition 8.17, we have

Λ_{M} ≅ Λ_{î_{R}⊙U_{Col(M)}⊙î_{S}} ≅ Λî_{S} ∘ Λî_{R} ≅ Δ_{i_{S}} ∘ Σ_{i_{R}}

and dually for the right adjoint Γ_{M}.

8.35. Corollary. Suppose that R and S be schemas. Let � ⊆ ℒ Adj_{Type}(R-Inst, S-Inst) [resp. let � ⊆ ℛ Adj_{Type}(S-Inst, R-Inst)] denote the full subcategory spanned by functors of the form Δ_{G} ∘ Σ_{F} [resp. of the form Π_{G} ∘ Δ_{F}]. This inclusion is an equivalence of categories.

Proof. The inclusion functor is fully faithful by definition and essentially surjective by Corollary 8.34 and Theorem 8.10.

8.36. Remark. Corollary 8.35 says that every right adjoint between instance categories is naturally isomorphic to a right pushforward followed by a pullback, Δ∘Π. While we do not discuss the details here, there is a similar characterization of parametric right adjoints (a.k.a. local right adjoints) between instance categories.

Recall that a functor F: � → � is a parametric right adjoint if, for each object c ∈ �, the slice F/c: �/c → �/(F c) is a right adjoint, see e.g. [Web07]. In our setting, one can show that every parametric right adjoint between instance categories is naturally isomorphic to a functor of the form Σ_{dopf} ∘ Δ ∘ Π, where the left pushfoward is along a discrete op-fibration, as discussed in Section 7.11. This generalizes the analogous fact for parametric right adjoints between presheaf categories, as shown in [Web07, Remark 2.12].

8.37. Bimodules presentation. We conclude Section 8 by discussing presentations of bimodules, which work very similarly to presentations of profunctors (Definition 4.45). Recall also the definition of schema presentations, Definition 5.6. Suppose that Type ≅ Cxt_{Σ}/E_{Σ} has algebraic signature Σ;^{6} see Definition 4.18.

8.38. Definition. Let R and R′ be schemas given respectively by presentations (Ξ, E_{e}, E_{o}) and (Ξ′, E′_{e}, E′_{o}). These present entity category R_{e} ≅ Fr(G_{Ξ})/E_{e} and observables profunctor R_{o} ≅ κ[Υ_{Ξ}]/E_{o}, and similarly for R′.

A bimodule signature Ω = (Ω_{e}, Ω_{o}) from Ξ to Ξ′ is a pair where Ω_{e} is a profunctor signature from G_{Ξ} to G_{Ξ′}, and Ω_{o} is a profunctor signature from G_{Ξ} to Σ.

A bimodule signature has an associated algebraic signature Ω̃ = (SΩ̃, ΦΩ̃), where

SΩ̃ = (G_{Ξ})_{0} ⊔ (G_{Ξ′})_{0} ⊔ S_{Σ}
ΦΩ̃ = (G_{Ξ})_{1} ⊔ (G_{Ξ′})_{1} ⊔ Φ_{Σ} ⊔ Υ_{Ξ} ⊔ Υ_{Ξ′} ⊔ Ω_{e} ⊔ Ω_{o}.

Say that a set E_{Ω} of equations over Ω̃ is a set of bimodule equations if for each equation Γ ⊢ (t_{1} = t_{2}) : s′ of E_{Ω}, the context is a singleton Γ = (x : s) with s ∈ (G_{Ξ})_{0} and s′ ∈ (G_{Ξ′})_{0} ⊔ S_{Σ}. We can partition the set E_{Ω} = (E_{Ω})_{e} ⊔ (E_{Ω})_{o}, where (E_{Ω})_{e} contains all equations where s′ ∈ (G_{Ξ′})_{0}, and (E_{Ω})_{o} contains all equations where s′ ∈ S_{Σ}.

Given a pair (Ω, E_{Ω}), consider the category CxtΩ̃/EΩ̃, where

EΩ̃ = E_{e} ∪ E_{o} ∪ E′_{e} ∪ E′_{o} ∪ E_{Ω}.

The bimodule M = κ[Ω]/E_{Ω} presented by (Ω, E_{Ω}) is defined as follows:

• for any objects r ∈ R̃ and s ∈ R̃′, the set M(r, r′) is defined to be the hom-set (CxtΩ̃/EΩ̃)(r, s),

• the functorial actions are given by substitution.

8.39. Remark. The presented bimodule M = κ[Ω]/E_{Ω} may be easier to understand in terms of its collage. We will write Col(Ω) = (G_{Col(Ω)}, Υ_{Col(Ω)}) for the following schema presentation:

(G_{Col(Ω)})_{0} = (G_{Ξ})_{0} ⊔ (G_{Ξ′})_{0}
(G_{Col(Ω)})_{1} = (G_{Ξ})_{1} ⊔ (G_{Ξ′})_{1} ⊔ Ω_{e}
Υ_{Col(Ω)} = Υ_{Ξ} ⊔ Υ_{Ξ′} ⊔ Ω_{o}.

It is easy to see that the algebraic signature { \atop Col(Ω)} corresponding to the schema signature Col(Ω) as in Definition 5.6 is precisely the same as the signature Ω̃ given above. Moreover, the collage Col(M) of the bimodule M is presented by (Col(Ω), E_{e} ∪E′_{e} ∪(E_{Ω})_{e}, E_{o} ∪E′_{o} ∪ (E_{Ω})_{o}).

The inclusions i_{R} and i_{S} of the schemas R and S into the collage Col(M) are also easy to understand in terms of this presentation, as they are both inclusions on the level of generators and equations as well.

6Signatures Σ should not be confused with data migration functors Σ_{−}.

8.40. Example. Let F = (F_{e}, F_{o}): R → S be a schema morphism. Both its companion F̂ and its conjoint F̂ have very simple presentations.

The generators of F̂: R S are ψ_{r}: r → F_{e}(r) for each r ∈ R_{e}. For each edge f: r → r′ in R there is an equation x.f.ψ_{r′} = x.ψ_{r}.F_{e}(f), and for each attribute att: r → τ in R there is an equation x.att = x.ψ_{r}.F_{o}(att), both in context (x : r).

The generators of F̂: S R are ϕ_{r}: F_{e}(r) → r for each r ∈ R_{e}. For each edge f: r → r′ in R there is an equation x.ϕ_{r}.f = x.F_{e}(f).ϕ_{r′}, and for each attribute att: r → τ in R there is an equation x.ϕ_{r}.att = x.F_{o}(att), both in context (x : F_{e}(r)).

9. Queries and uber-queries

In this section, we will employ many of the concepts and operations studied so far in order to describe the process of querying an algebraic database. We will also give examples that tie in with running examples from previous sections.

A query is a question asked of a database, such as "Tell me the set of employees whose manager is named Alice". Queries are often written using "Select-From-Where" — e.g. in the database query language SQL — or equivalently using "For-Where-Return" syntax. This syntax both poses the question and provides a table layout in which to record the results.

In our current setting, we will express a query on a given S-instance J, by constructing a new schema R and a bimodule M: R S. Running the query will amount to applying the functor Γ_{M}: S-Inst → R-Inst from (37). Classically, a For-Where-Return query returns a single table (with no foreign keys), so the result schema R has a very specific form; namely, its entity side is the terminal category, R_{e} = {∗}.

If we allow arbitrary R and arbitrary bimodules R S, the "query" Γ_{M} could be thought of as a method of migrating data from S to R, but it could also be considered as a collection of queries and homomorphisms between them; we refer to such a setup as an uber-query. We will discuss this interpretation of bimodules in Section 9.8.

9.1. Queries. We begin by discussing the usual For-Where-Return queries and how they appear in our setup.

9.2. Definition. Let S be a schema given by a presentation (Ξ, E), see Definition 5.6. A query on S is a 4-tuple Q = (Q_{f}, Q_{w}, Q_{a}, Q_{r}), where Q_{f} is a context over Ξ̃, Q_{w} is a set of equations in Q_{f}, Q_{a} is a context over (the signature of) Type, and Q_{r}: Q_{f} → Q_{a} is a context morphism over Ξ̃.

We will adopt the For-Where-Return notation for presenting the data of a query as defined in Definition 9.2, as follows:

FOR: Q_{f}
WHERE: Q_{w}
RETURN: Q_{r}

This notation is sometimes called flower syntax (an acronym of For-Let-Where-Return) or comprehension syntax [AHV95].

9.3. Example. Let S be the schema from Example 5.8. We give an example query Q on S:

FOR: e : Emp, d : Dept
WHERE: e.wrk.name = Admin,

(e.sal ≤ d.sec.sal) = ⊤

RETURN: emp_last := e.last

                                  dept_name := d.name
                                  diff := d.sec.sal − e.sal

In this query, Q_{f} is the context (e : Emp, d : Dept), Q_{w} is the set containing the two equations at the WHERE clause, Q_{a} is the context (emp_last : Str, dept_name : Str, diff : Int), and Q_{r}: Q_{f} → Q_{a} is the context morphism (Definition 4.11) displayed in the RE-TURN clause.

9.4. Query bimodules. Any query Q on a schema S gives rise to a schema R and bimodule M: R S. The schema R is free on the schema signature (G, Υ), where G is the graph with one node ∗ and no edges, and Υ has one function symbol, i.e. generating attribute x: ∗ → τ, for each variable x : τ in Q_{a}. Note that the entity category R_{e} is terminal, hence R_{o} : R_{e} Type can be identified with a single Type-algebra, the free algebra R_{o} = κ[Q_{a}]. We may refer to R as the result schema.

Using Proposition 8.24, the data of any M: R S is equivalent to a single S-instance M_{o}(∗) denoted M_{o}, together with a morphism of Type-algebras M_{r} : κ[Q_{a}] → (M_{o})_{t}. Equivalently, by Σ_{!_{S}} ⊣ Δ_{!_{S}} this is a morphism of S-instances M_{r} : Σ_{!_{S}}κ[Q_{a}] = ⟨Q_{a}⟩ → M_{o}, using Remark 7.5 and Definition 6.13.

We thus define M_{o} = ⟨Q_{f}⟩/Q_{w}, precisely presented by the first two clauses of the flower syntax, while M_{r} is given by the context morphism Q_{r} of the last clause (see Definition 4.32). Following standard database theory, we refer to M_{o} = ⟨Q_{f}⟩/Q_{w} as the frozen instance of the query Q.

The bimodule M associated to Q in turn determines a functor Γ_{M}: S-Inst → R-Inst; we will abuse notation by writing it as Γ_{Q}. It is this functor which carries out the operation of “querying an S-instance using Q”. As the result schema R has a single entity, the output of this functor can be seen as a single table containing the results of the query, with one column for each variable in Q_{a}.

9.5. Example. Let S and Q be as in Example 9.3. The query Q determines a schema R and a bimodule M: R S as follows. The schema R has a single entity — call it “∗” — and attributes emp_last, dept_name: ∗ → Str, and diff: ∗ → Int coming from Q_{a}.

The bimodule M is determined by the frozen instance M_{o} = ⟨e : Emp, d : Dept⟩/Q_{w}, where Q_{w} contains the two equations from Example 9.3, together with the morphism

M_{r} : ⟨emp_last, dept_name : Str, diff : Int⟩ → ⟨e : Emp, d : Dept⟩/Q_{w}

given by the context morphism

     [emp_last := e.last, dept_name := d.name, diff := d.sec.sal − e.sal].

Note that the schema R is isomorphic to the one from Example 5.14, and that the frozen instance M_{o} is the instance from Example 6.16.

Let J ∈ S-Inst be the instance from Example 6.3. We will now compute the result Γ_{Q}(J) ∈ R-Inst of querying J with Q. On the single entity of R, we have by (37) that (Γ_{Q}J)(∗) = S-Inst(M_{o}, J), and we saw in Example 6.17 that this set has three elements. The Type-algebra (Γ_{Q}J)_{t} is the same as J_{t}, by (38). The values of the attributes of R are determined using the morphism M_{r}:

(Γ_{Q}J)(∗) = S-Inst( ⟨Q_{f}⟩/Q_{w}, J ) ⟶ S-Inst( ⟨Q_{a}⟩, J ) ≅ ∏_{(x:τ)∈Q_{a}} J_{t}(τ).  (49)

A transform ⟨Q_{f}⟩ → J has an underlying context morphism Φ → Q_{f}, where Φ is the context of the canonical presentation of J (see Remark 6.15). We can express (49) using context morphisms: given a transform ⟨Q_{f}⟩/Q_{w} → J corresponding to an element of (Γ_{Q}J)(∗), simply compose its underlying context morphism Φ → Q_{f} with Q_{r}: Q_{f} → Q_{a}. The attributes of this row of the table “∗” can be read off of the resulting context morphism Φ → Q_{a}.

Doing this, we obtain the result

                        ∗ emp_last  dept_name  diff

1 Noether  HR  100
2 Euclid  HR  150
3 Euclid  Admin  0

(Note that the row-ids are arbitrary.) For example, the first row corresponds to the transform ⟨Q_{f}⟩ → J given by [e := e2 , d := d1 ]. Composing this with Q_{r} gives

[emp_last := e2 .last, dept_name := d1 .name, diff := d1 .sec.sal − e1 .sal], which

simplifies to the first row of the table above.

9.6. Remark. By Corollary 8.34, the result of any query Q on S, with result schema R and associated bimodule M, is equivalently obtained as the composite of data migration functors

S-Inst  Col(M)-Inst  R-Inst
J  Π_{i_{S}}(J)  Δ_{i_{R}}(Π_{i_{S}}(J)) ≅ Γ_{Q}(J)

Π_{iS}

Δ_{i_{R}} (50)

where the schema mappings i_{R} : R → Col(M) ← S :i_{S} into the bimodule collage Col(M) are as in Section 8.29.

For example, the query in Example 9.5 gave the same result as we found using Examples 7.8 and 7.10. One can check that the bimodule collage is Col(M) ≅ T given in (25), and the mappings F, G of the mentioned examples are the collage inclusions. Hence this is an instance of (50).

9.7. Remark. In practice, one would like a guarantee that a query result Γ_{Q}(J) is finite whenever J is finite. To achieve this, one has to place the extra condition on the query Q that only entities — no types — appear in Q_{f}. This condition also ensures the domain independence [AHV95] of the query, meaning that it is not necessary to enumerate the elements of a type to compute the query result.

9.8. Uber-queries. If queries correspond to (R, S)-bimodules where R has only one entity, then we need a name for more general bimodules; we call them uber-queries. An uber-query is roughly a diagram of queries. The morphisms in this diagram will be called Keys, and our syntax is accordingly extended to be of the form For-Where-Keys-Return.

9.9. Example. To describe a bimodule of the following form

            A A' Int Str Bool dept_name diff f last Dept Emp Int Str Bool wrk mgr sal last sec name plus eqs from (25) S L N

we will need two instances I := N(A) and I′ := N(A′), and a transform N(f): I′ → I between them, as well as three terms diff, name, last of the specified types in I and I′. Indeed, this gives a functor L̃^{op} → S-Inst (where objects Int, Str, and Bool in the type side are sent to the corresponding representable instances, as usual; Definition 8.3).

In Example 6.18, we constructed two S-instances and a transform I′ → I between them . We will rewrite them, together with the three terms, in For-Where-Keys-Return syntax below.

A′ =  A =
FOR: e′ : Emp  FOR: e : Emp, d : Dept
WHERE: e′.wrk.name = Admin  WHERE: e.wrk.name = Admin

            e′.sal ≤ e′.wrk.sec.sal  e.sal ≤ d.sec.sal

KEYS: f := Emp[e := e′, d := e′.wrk]
RETURN: last := e′.last  RETURN: dept_name := e.wrk.name

                                               diff := d.sec.sal − e.sal

For any S-instance J, we can apply Γ_{N}: S-Inst → L-Inst. If J is as in Example 6.3, then Γ_{N}(J) is the following L-instance:

                     A’ last   f

0 Euclid 3

                                       A  dept_name  diff

1  HR  100
2  HR  150
3  Admin  0

10. Implementation

The mathematics developed in this paper has been implemented using OPL, an Operadic Programming Language, which can be can be downloaded from http://categoricaldata.net/fql.html. The examples in this paper are pre-loaded as the “Paper” example in the software package. In this section we briefly discuss implementation issues that arise, namely in negotiating between syntactic presentations (e.g. those discussed in Section 4) and the objects they denote.

Most constructions involving finitely-presented categories, including query evaluation and collage construction, depend crucially on solving word problems in categories, and these problems are not in general decidable. In Section 10.1 we describe our approach to solving word problems, and in Section 10.2 we describe how we use word problems to compute collages and evaluate queries.

10.1. Solving Word Problems. Given a category presentation (G, E) as described in Section 4.35, the word problem is to decide if two terms (words) in G are equivalent under E. The word problem is obviously semi-decidable: to prove if two terms p and q in G are equal under E, we can systematically enumerate all of the (usually infinite) consequences of E until we find p = q. However, if p and q are not equal, then this enumeration will never stop. In practice, not only is enumeration computationally infeasible, but for query evaluation and collage construction, we require a true decision procedure: an algorithm which, when given p and q as input, will always terminate with “equal” or “not equal”. Hence, we must look to efficient, but incomplete, automated theorem proving techniques to decide word problems.

The OPL tool allows any theorem prover to be used to decide word problems. In addition, the OPL tool also provides a default, built-in theorem prover based on Knuth-Bendix completion [KB70]: from (Σ, E), it attempts to construct a system of re-write rules (oriented equations), R, such that p and q are equal under E if and only if p and q re-write to syntactically equal terms (so-called normal forms) under R. We demonstrate this with an example. Consider a presentation of the algebraic theory of groups, on the left, below. Knuth-Bendix completion yields the re-write system on the right, below: ^{7}

7Because there is only one sort, say S_{Σ} = {G}, we drop the contexts in the Axiom side. For example, the second equation — axiom — should be x : G ⊢ (x^{−1} ∗ x = 1) : G, according to Section 4.

Axioms  Re-write rules
1 ∗ x = x  1 ∗ x ⇝ x
x^{−1} ∗ x = 1  x^{−1} ∗ x ⇝ 1
(x ∗ y) ∗ z = x ∗ (y ∗ z)  (x ∗ y) ∗ z ⇝ x ∗ (y ∗ z)
x^{−1} ∗ (x ∗ y) ⇝ y
1^{−1} ⇝ 1
x ∗ 1 ⇝ x
(x^{−1})^{−1} ⇝ x
x ∗ x^{−1} ⇝ 1
x ∗ (x^{−1} ∗ y) ⇝ y
(x ∗ y)^{−1} ⇝ y^{−1} ∗ x^{−1}

To see how these re-write rules are used to decide the word problem, consider the two terms (a^{−1} ∗ a) ∗ (b ∗ b^{−1}) and b ∗ ((a ∗ b)^{−1} ∗ a). Both of these terms re-write to 1 under the above re-write rules; hence, we conclude that they are equal. In contrast, the two terms 1 ∗ (a ∗ b) and b ∗ (1 ∗ a) re-write to a ∗ b and b ∗ a, respectively, which are not syntactically the same; hence, we conclude that they are not equal.

The details of how the Knuth-Bendix algorithm works are beyond the scope of this paper. However, we make two remarks. First, Knuth and Bendix’s original algorithm ([KB70]) can fail even when a re-write system to decide a word problem exists; for this reason, we use the more modern, “unfailing” variant of Knuth-Bendix completion [BDP89]. Second, we remark that Buchberger’s algorithm for computing Gröbner bases is a very similar algorithm used in many computer algebra systems, and it may be seen as the instantiation of the Knuth-Bendix algorithm in the theory of polynomial rings [Mar96].

10.2. Saturation and Query Evaluation. Given a category presentation (G, E), a decision procedure for the word problem allows us to (semi) compute the category � that (G, E) presents. To do this, we construct � in stages: first, we find all non-equal terms of size 0 in G; ^{8} call this �^{0}. Then, we add to �^{0} all non-equal terms of size 1 that are not equal to a term in �^{0}; call this �^{1}. We iterate this procedure, obtaining a sequence �^{0}, �^{1}, . . .. If � is indeed finite, then there will exist some n such that �^{n} = �^{n+1} = � and we can stop. Otherwise, our attempt to construct � will run forever: it is not decidable whether a given presentation (G, E) generates a finite category. The category � will be isomorphic to the category Fr(G)/E obtained by quotienting the free category on G by the equations in E (Definition 4.41); essentially, � represents equivalence classes of terms by a smallest possible representative, as explained in detail in Section 4. (Note that the normal forms chosen by the internal Knuth-Bendix theorem prover for the purposes of deciding the word problem need not in general be the same as the chosen representatives of equivalences classes in �.)

Most uses of the OPL tool involve saturating instance presentations into collages so that they may be examined as tables (e.g. Example 6.16). This just means replacing part of the presentation with a canonical presentation (see Remarks 4.21, 4.34 and 6.15^{9}) The saturation process is very similar to the process described in the preceding paragraph, with one small difference. In general, the ‘type side’ of the collage (see Remark 5.3) will denote an infinite category. For example, if Type is the free group on one generator {a}, it will contain a, a ∗ a, a ∗ a ∗ a, and so on. Hence, it is usually not possible to saturate the type side of an instance. So, the OPL tool saturates only the entity side of an instance, which will often be finite in practice. From the saturated entity side presentation and a set of rewrite rules for the collage, it is possible to construct a set of tables that faithfully represent the instance. The tables for the entity side of the instance are simply a tabular rendering of the finite category corresponding to the saturated entity side of the instance’s collage (� in the preceding paragraph). The tables for the attributes of the instance must also contain representatives of equivalence classes of terms, but unlike the entity side case, where representatives are chosen based on size, it is less clear which representative to choose. For example, there is an implicit preference to display 1,024 instead of 2^{10}, even though the size (as defined in the previous footnote) of the former is greater than the size of the latter. The OPL tool allows these representatives to be computed by external programs, thereby providing a “hook” for the tool to interface with other programming languages and systems. For example, users can provide a Java implementation of natural numbers for the commutative ring type side used in this paper, and the java compiler will normalize terms like 2^{10} into 1024. By default, the OPL tool will display the normal forms computed by the internal Knuth-Bendix theorem prover in the attribute tables.

8By the size of a term, we mean the height of the associated syntax tree. For example max(x.sal, x.mgr.sal) has size of three.

To evaluate a query Q such as that in Example 9.5 on a presented instance I, we first saturate the entity side of I as described in the preceding paragraph. Evaluation of the query, Γ_{Q}(I) as in Section 9.4, proceeds similarly to evaluation of ‘For-Where-Return’ queries in traditional SQL systems [AHV95]: first, we compute a (typically large) set of tuples corresponding to the FOR clause by repeatedly looping through I. Then, we filter this set of tuples by the WHERE clause; here we must be sure to decide equality of tuples under the equational theory for I, using Knuth-Bendix as described above. Finally, we project out certain components of these tuples, according to the RETURN clause. The result of the query will be a saturated instance, which has a canonical presentation as in Remark 6.15.

The OPL tool’s tabular rendering of the instance from Example 6.3 is shown in Fig. 7. Because a unary representation of the integers is computationally inefficient, for expediency the employee salaries in the OPL program have been reduced compared to Example 6.3. A more efficient axiomatization of the integers, such as using binary, can also be used.

9For explanatory reasons these particular examples saturate a frozen instance associated with a query, but the implementation does not need to saturate frozen instances to evaluate queries.

Figure 7: OPL displaying the instance from Example 6.3

A. Componentwise composition and exponentiation in �ata

We defined composition of bimodules and 2-cells in (40) and (41) and exponentiation of bimodules in Proposition 8.16. In Proposition 8.20 we saw that bimodules can be equivalently defined in several components, separating the entity and type sides of the structure. It is natural to ask what composition and exponentiation (and as special cases, the data migration functors) look like in this decomposed view.

In fact, when first working out the ideas presented in this paper, we used componentwise formulas to understand all the constructions. In writing it up, we decided that the coend formulas were more succinct and often easier to work with; however, the machinery below still turns out to be useful in certain cases, so we present it without proof for the interested reader.

Recall the left tensor ⊗ defined in Definition 3.11, which ‘preserves algebraicity’ of profunctors on the right.

A.1. Proposition. The composition M ⊙ N of two bimodules R ^{M} S ^{N} T in �ata (40) is equivalently given in components as follows: (M ⊙ N)_{e} = M_{e} ⊙ N_{e} in �rof, and the rest of the components are given using a pushout, as in the following diagram in the category [R_{e}^{op}, Type-Alg]:

R_{o}  M_{e} ⊗ S_{o}  M_{e} ⊗ N_{e} ⊗ T_{o}

M_{t}  M_{e} ⊗ N_{t}

M_{r} (M ⊙ N)_{t} (M⊙N)_{r} M_{o} M_{e}⊗N_{r} ⌜ M_{e}⊗N_{o} (M⊙N)_{o}

This follows from the following lemma, which can be proven using Proposition 2.25:

A.2. Lemma. Let L: A_{0} A_{1}, M: B_{0} B_{1}, and N: C_{0} C_{1} be proarrows in an equipment � with extensive collages and local finite colimits. Let X ∈ _{L}Simp_{M} and Y ∈ MSimp_{N} be simplices, and let P: L̃ M̃ and Q: M̃ Ñ be proarrows such that X ≅ LRes_{M}(P) and Y ≅ _{M}Res_{N}(Q) (see Section 2.22). Then the components of _{L}Res_{N}(P ⊙Q) can be computed by pushout:

\begin{matrix}X_{i,0} ⊙ M ⊙ Y_{1,j} & X_{i,0} ⊙ Y_{0,j} \\ X_{i,1} ⊙ Y_{1,j} & î_{A_{i}} ⊙ (P ⊙ Q) ⊙ î_{C_{j}} \end{matrix} ; ⌜ (51)

Moreover, the 2-cells of _{L}Res_{N}(P ⊙ Q) are found using these pushouts in an evident way.

A.3. Proposition. The horizontal composition of 2-cells in �ata

\begin{matrix}R & S & T \\ R′ & S′ & T′ \end{matrix} M F N G H M′ N′ ⇓θ ⇓ϕ

is given (Proposition 8.22) by (θ ⊙ ϕ)_{e} = θ_{e} ⊙ ϕ_{e}, while (θ ⊙ ϕ)_{t} is induced by the diagram

M_{t}  M_{e} ⊗ S_{o}  M_{e} ⊗ N_{t}

F̂_{e} ⊗ M′_{t}  F̂_{e} ⊗ M′_{e} ⊗ S′_{o}  F̂_{e} ⊗ M′_{e} ⊗ N′_{t} θ_{t} θ_{e}⊗G_{o} M_{o} M_{e}⊗N_{r} θ_{e}⊗ϕ_{t} id ⊗M′_{o} id ⊗M′_{e}⊗N′_{r}

where (M ⊙ N)_{t} and (M′ ⊙ N′)_{t} are the pushouts of the top and bottom rows respectively, by Proposition A.1.

A.4. Proposition. Let N: S T and P: R T be bimodules. The bimodule N ▷ P: R S is given as follows: the entity component (N ▷ P)_{e} is computed by a pointwise pullback, for any objects s ∈ S_{e}, r ∈ R_{e},

(N ▷ P)_{e}(r, s)  Set^{T_{e}}(N_{e}(s, –), P_{e}(r, –))

Set^{T_{e}}(N_{e}(s, –), Type-Alg(T_{o}(–), P_{t}(r)))

Type-Alg(N_{t}(s), P_{t}(r))  Type-Alg((N_{e} ⊗ T_{o})(s), P_{t}(r)).

⌟

P_{o}

≅
N_{o}

Equivalently, (N ▷P)_{e}(r, s) = T-Inst(N(s), P (r)). The other components are (N ▷P)_{t} = P_{t}, (N ▷ P)_{r} = P_{r}, and (N ▷ P)_{o} is the composition

(N ▷ P)_{e} ⊗ S_{o} → Type-Alg(N_{t}(–), P_{t}(–)) ⊗ N_{t} → P_{t}.

References

[AHV95] Serge Abiteboul, Richard Hull, and Victor Vianu. Foundations of Databases. Addison-Wesley, 1995. isbn: 0-201-53771-0.

[AR94] Jiří Adámek and Jiří Rosický. Locally presentable and accessible categories. London Mathematical Society Lecture Note Series 189. Cambridge University Press, 1994. isbn: 0-521-42261-2.

[ARV11] J. Adámek, J. Rosický, and E. M. Vitale. Algebraic theories. Cambridge Tracts in Mathematics 184. Cambridge University Press, 2011. isbn: 978-0-521-11922-1.

[BDP89] L. Bachmair, N. Dershowitz, and D.A. Plaisted. “Completion Without Failure”. In: Resolution of Equations in Algebraic Structures - Rewriting Techniques 2 (1989), pp. 1–30.

[Bén00] Jean Bénabou. “Distributors at work”. Lecture notes written by Thomas Stre-

icher. 2000. url: http://www.mathematik.tu-darmstadt.de/~streicher/FIBR/DiWo.pdf.

[Bor94a] Francis Borceux. Handbook of categorical algebra. Vol. 1: Basic category theory. 3 vols. Encyclopedia of Mathematics and its Applications 50. Cambridge University Press, 1994. isbn: 0-521-44178-1.

[Bor94b] Francis Borceux. Handbook of categorical algebra. Vol. 2: Categories and structures. 3 vols. Encyclopedia of Mathematics and its Applications 51. Cambridge University Press, 1994. isbn: 0-521-44178-1.

[BW85] Michael Barr and Charles Wells. Toposes, Triples and Theories. A Series of Comprehensive Studies in Mathematics 278. Springer-Verlag, 1985. isbn: 0-387-96115-1.

[DHI12] AnHai Doan, Alon Halevy, and Zachary Ives. Principles of Data Integration. 1st. San Francisco, CA, USA: Morgan Kaufmann Publishers Inc., 2012. isbn: 0124160441, 9780124160446.

[FGR03] Michael Fleming, Ryan Gunther, and Robert Rosebrugh. “A database of categories”. In: Journal of Symbolic Computation 35.2 (Feb. 2003), pp. 127–135.

issn: 0747-7171. doi: 10.1016/S0747-7171(02)00104-9.

[GP04] Marco Grandis and Robert Paré. “Adjoint for double categories”. In: Cahiers de Topologie et Géométrie Différentielle Catégoriques 45.3 (2004), pp. 193– 240.

[GS15] Richard Garner and Michael Shulman. Enriched categories as a free cocompletion. Nov. 2015. arXiv: 1301.3191v2 [math.CT].

[Hun04] Edward V. Huntington. “Sets of independent postulates for the algebra of logic”. In: Transactions of the American Mathematical Society 5.3 (1904),

pp. 288–309. doi: 10.1090/s0002-9947-1904-1500675-4.

[Jac99] Bart Jacobs. Categorical logic and type theory. Vol. 141. Studies in Logic and the Foundations of Mathematics. North-Holland Publishing Co., Amsterdam, 1999, pp. xviii+760. isbn: 0-444-50170-3.

[JR02] Michael Johnson and Robert Rosebrugh. “Sketch Data Models, Relational Schema and Data Specifications”. In: Electronic Notes in Theoretical Computer Science 61 (2002). CATS’02, Computing: the Australasian Theory Symposium, pp. 51–63. issn: 1571-0661.

[KB70] Donald Knuth and Peter Bendix. “Simple Word Problems in Universal Algebra”. In: Computational Problems in Abstract Algebra. Ed. by John Leech. Pergamon Press, 1970, pp. 263–297.

[Kel05] G. M. Kelly. “Basic concepts of enriched category theory”. In: Reprints in The-

ory and Applications of Categories 10 (2005). url: http://www.tac.mta.ca/tac/reprints/articles/10/tr10abs.html.

[Kel89] G.M. Kelly. “Elementary observations on 2-categorical limits”. In: Bulletin of the Australian Mathematical Society 39.02 (Apr. 1989), pp. 301–317. issn:

1755-1633. doi: 10.1017/S0004972700002781.

[Lei04] Tom Leinster. Higher operads, higher categories. London Mathematical Society Lecture Note Series 298. Cambridge University Press, Cambridge, 2004. isbn:

0-521-53215-9. doi: 10.1017/CBO9780511525896.

[Mac98] Saunders Mac Lane. Categories for the working mathematician. 2nd ed. Graduate Texts in Mathematics 5. New York: Springer-Verlag, 1998. isbn: 0-387-98403-8.

[Mar96] Claude Marché. “Normalized Rewriting: An Alternative to Rewriting Modulo a Set of Equations”. In: Journal of Symbolic Computation 21.3 (Mar. 1996), pp. 253–288. issn: 0747-7171. doi: 10.1006/jsco.1996.0011.

[Mat89] Hideyuki Matsumura. Commutative ring theory. Trans. from Japanese by M. Reid. 2nd ed. Cambridge Studies in Advanced Mathematics 8. Cambridge University Press, 1989. isbn: 0-521-36764-6.

[Mit96] John C. Mitchell. Foundations of Programming Languages. Cambridge, MA: MIT Press, 1996. isbn: 0-262-13321-0.

[MS08] Katherine Munn and Barry Smith. Applied ontology: an introduction. Vol. 9. Walter de Gruyter, 2008.

[nLab]  Nerve and realization. url: http://ncatlab.org/nlab/show/nerve+and+realization

(visited on 01/19/2016).

[RW92] Robert Rosebrugh and R. J. Wood. “Relational Databases and Indexed Categories”. In: Canadian Mathematical Society Conference Procedings. International Summer Category Theory Meeting. (June 23–30, 1991). Ed. by R. A. G. Seely. Vol. 13. American Mathematical Society, 1992, pp. 391–407.

[Sch15] Patrick Schultz. Regular and exact (virtual) double categories. 2015. arXiv:

1505.00712 [math.CT].

[Shu08] Michael Shulman. “Framed bicategories and monoidal fibrations”. In: Theory and Applications of Categories 20.18 (2008), pp. 650–738. arXiv: 0706.1286 [math.CT].

[Shu10] Michael Shulman. Constructing symmetric monoidal bicategories. 2010. arXiv:

1004.0993 [math.CT].

[Spi12] David I. Spivak. “Functorial data migration”. In: Information and Computation 127 (Aug. 2012), pp. 31–51. issn: 0890-5401. doi: 10.1016/j.ic.2012.05.001.

         arXiv: 1009.1166v4 [cs.DB].

[SW15] David I. Spivak and Ryan Wisnesky. “Relational Foundations for Functorial Data Migration”. In: Proceedings of the 15th Symposium on Database Programming Languages. DBPL 2015. Pittsburgh, PA: ACM, 2015, pp. 21–28. isbn: 978-1-4503-3902-5. doi: 10.1145/2815072.2815075.

[Web07] Mark Weber. “Familial 2-Functors and Parametric Right Adjoints”. In: Theory and Applications of Categories 18.22 (2007), pp. 665–732.

[Wis+15] Ryan Wisnesky, David I. Spivak, Patrick Schultz, and Eswaran Subrahmanian. Functorial Data Migration: From Theory to Practice. report G2015-1701. National Institute of Standards and Technology, 2015. arXiv: 1502.05947v2.

[Woo82] R. J. Wood. “Abstract pro arrows I”. In: Cahiers de Topologie et Géométrie Différentielle Catégoriques 23.3 (1982), pp. 279–290. issn: 0008-0004.

[Woo85] R. J. Wood. “Proarrows II”. In: Cahiers de Topologie et Géométrie Différentielle Catégoriques 26.2 (1985), pp. 135–168.

Massachusetts Institute of Technology, 77 Massachusetts Ave. Cambridge, MA 02139

Email: schultzp@mit.edu
      dspivak@mit.edu,
      cvasilak@mit.edu
      ryan@catinf.com
This article may be accessed at http://www.tac.mta.ca/tac/

THEORY AND APPLICATIONS OF CATEGORIES (ISSN 1201-561X) will disseminate articles that significantly advance the study of categorical algebra or methods, or that make significant new contributions to mathematical science using categorical methods. The scope of the journal includes: all areas of pure category theory, including higher dimensional categories; applications of category theory to algebra, geometry and topology and other areas of mathematics; applications of category theory to computer science, physics and other mathematical sciences; contributions to scientific knowledge that make use of categorical methods. Articles appearing in the journal have been carefully and critically refereed under the responsibility of members of the Editorial Board. Only papers judged to be both significant and excellent are accepted for publication. Full text of the journal is freely available from the journal’s server at http://www.tac.mta.ca/tac/. It is archived electronically and in printed paper format.

Subscription information Individual subscribers receive abstracts of articles by e-mail as they are published. To subscribe, send e-mail to tac@mta.ca including a full name and postal address. For institutional subscription, send enquiries to the Managing Editor, Robert Rosebrugh, rrosebrugh@mta.ca.

Information for authors The typesetting language of the journal is TEX, and L^{A}TEX2e is required. Articles in PDF format may be submitted by e-mail directly to a Transmitting Editor. Please obtain detailed information on submission format and style files at http://www.tac.mta.ca/tac/.

Managing editor. Robert Rosebrugh, Mount Allison University: rrosebrugh@mta.ca

TEXnical editor. Michael Barr, McGill University: barr@math.mcgill.ca

Assistant TEX editor. Gavin Seal, Ecole Polytechnique Fédérale de Lausanne:

gavin_seal@fastmail.fm

Transmitting editors.

Clemens Berger, Université de Nice-Sophia Antipolis: cberger@math.unice.fr Richard Blute, Université d’ Ottawa: rblute@uottawa.ca Lawrence Breen, Université de Paris 13: breen@math.univ-paris13.fr Ronald Brown, University of North Wales: ronnie.profbrown(at)btinternet.com Valeria de Paiva: Nuance Communications Inc: valeria.depaiva@gmail.com Ezra Getzler, Northwestern University: getzler(at)northwestern(dot)edu Kathryn Hess, Ecole Polytechnique Fédérale de Lausanne: kathryn.hess@epfl.ch Martin Hyland, University of Cambridge: M.Hyland@dpmms.cam.ac.uk Anders Kock, University of Aarhus: kock@imf.au.dk Stephen Lack, Macquarie University: steve.lack@mq.edu.au F. William Lawvere, State University of New York at Buffalo: wlawvere@buffalo.edu Tom Leinster, University of Edinburgh: Tom.Leinster@ed.ac.uk Ieke Moerdijk, Utrecht University: i.moerdijk@uu.nl Susan Niefield, Union College: niefiels@union.edu Robert Paré, Dalhousie University: pare@mathstat.dal.ca Jiri Rosicky, Masaryk University: rosicky@math.muni.cz Giuseppe Rosolini, Università di Genova: rosolini@disi.unige.it Alex Simpson, University of Ljubljana: Alex.Simpson@fmf.uni-lj.si James Stasheff, University of North Carolina: jds@math.upenn.edu Ross Street, Macquarie University: ross.street@mq.edu.au Walter Tholen, York University: tholen@mathstat.yorku.ca Myles Tierney, Université du Québec à Montréal : tierney.myles4@gmail.com R. J. Wood, Dalhousie University: rjwood@mathstat.dal.ca