Imagining Bicomodules with Type Theory

type theory

polynomial functors

Author

Joshua Meyers

Published

2022-08-19

Abstract

Some say that the objects of mathematics really exist in some Platonic realm, and some say they are fictions in the minds of mathematicians. Either way, it is evident that they cannot be directly grasped with the ordinary five senses. Nobody has ever seen a perfect circle or a natural number. Rather, we grasp the objects of mathematics by means of imagination. I set out to imagine bicomodules in Poly (aka prafunctors) in this way, as they are an important and powerful feature of the Poly ecosystem. This blog post shows what I have come up with. As it turned out, the result is not only suitable for imagination, but also for implementation in computers (digital imagination, perhaps?) Indeed, we’ll see bicomodules as an essentially algebraic theory and discuss how it is used for data migration.

1 Introduction

It is possible to get quite far in math by formally reasoning about objects inadequately imagined. This is Terence Tao’s “rigorous” stage of mathematical education. But the “post-rigorous” stage is attained when this formal reasoning has been used to refine the imagination so much that it never conflicts with the reasoning. Thus “unintuitive” facts become intuitive, and can be ‘seen’’ to be true with the imagination directly.

I set out to imagine bicomodules in \textsf{Poly} (aka prafunctors) in this way, as they are an important and powerful feature of the \textsf{Poly} ecosystem. This blog post shows what I have come up with. As it turned out, the result is not only suitable for imagination, but also for implementation in computers (digital imagination, perhaps?) Indeed, we’ll see bicomodules as an essentially algebraic theory and discuss how it is used for data migration.

2 Comonoids

Let c and d be comonoids in \textsf{Poly}, i.e. categories. How can we then imagine a bicomodule c\triangleleft\!\!\overset{m}{\sout{\,\,\phantom{m}\,\,}}\!\!\triangleleft d?

First, let us recall how comonoids in \textsf{Poly} model categories. It is actually easier to see how a category is a comonoid in \textsf{Poly}. Let C be a category, and consider the polynomial c\coloneqq \sum_{I\in \textrm{Ob}(C)}\mathcal{y}^{\;\sum\limits_{J\in \textrm{Ob}(C)}C(I,J)}=\sum_{I\in \textrm{Ob}(C)}\prod_{J\in \textrm{Ob}(C)}\mathcal{y}^{C(I,J)}. In words, the positions c(1) of this polynomial are the objects of C and the directions at one of these objects are all of its outgoing morphisms. This polynomial underlies the comonoid which models the category C.

Notice the asymmetry inherent in this picture — we could have said that directions were ingoing morphisms. Thus categories actually can be modeled as comonoids in \textsf{Poly} in two, dual ways. (In fact, if we raise the size issues that are usually bracketed, we obtain two slightly different classes of categories. Considering directions as outgoing morphisms, we obtain locally small categories such that for each object I, the class \{J\in\textrm{Ob}(C)\mid C(I,J)\textrm{ nonempty}\} is a set. Considering directions as ingoing morphisms, we obtain a dual condition.)

Now what is the comonoid structure? First, the counit \epsilon:c\to y gives us the identity morphisms of C. The map on positions is the unique map \textrm{Ob}(C)\to 1 and the map on directions sends, for I\in\textrm{Ob}(C), the unique element of 1 to \mathop{\mathrm{id}}_I.

Secondly, the comultiplication \delta:c\to c\mathbin{\triangleleft}c tells us about codomains and composition. Recall that c\mathbin{\triangleleft}c has positions \Sigma_{I\in c(1)}c(1)^{c[I]} and the directions of a position (I\in c(1), J: c[a]\to c(1)) are pairs (f:c[I], f':c[Jf]). So \delta acts on positions by sending I\in\textrm{Ob}(C) to (I,\textrm{cod}_I:c[I]\to c(1)), where \textrm{cod}_I is the codomain map, sending morphisms with domain I to their codomains. Given a position I\in\textrm{Ob}(C), the morphism \delta acts on directions by sending (f:c[I], f':c[\textrm{cod}_I(f)]) to the composition f; f'\in c[I]. It is straightforward (but not necessarily quick) to check that the comonoid laws enforce the identity and associativity laws of C, and that any comonoid in \textsf{Poly} will arise from a category in this way.

3 Bicomodules

Now we consider a bicomodule c\triangleleft\!\!\overset{m}{\sout{\,\,\phantom{m}\,\,}}\!\!\triangleleft d. First we consider the left action m \to c\mathbin{\triangleleft}m. We start by restricting to the the simple case in which m is a constant polynomial (a set of positions), so we have simply m\to c(m).

Each position P\in m is hereby sent to a position (I_P\in c(1), Q_P:c[I]\to m) of c(m). In words, each position P of m is sent to an object I_P of C, then for each morphism f coming out of that object, we obtain a new position Q_P(f) of m. We consider the first part of this description a typing of m by objects of C, and we write P:I to denote that P is sent to the object I=I_P. We consider the second part of the description a right action, and we write P.f to denote the position Q_f(I).

It is straightforward (though not necessarily quick) to show that the comodule axioms guarantee the following rules: \frac{(P\in m):(I\in c(1)),\ f:I\to I'}{P.f:I'} \qquad \frac{P:I}{P.\mathop{\mathrm{id}}_I=P} \qquad \frac{P:I,\ f:I\to I,\ f':I\to I''}{P.(f; f')=(P.f).f'}

This is actually nothing else than a copresheaf on C, i.e. a C-set.

[It is a point worth stopping to consider if you have not encountered it already that a C-set can be described this way, as a set typed by objects of C and with a right action by morphisms of C. This interpretation of C-sets also provides a very intuitive analysis of the Yoneda Lemma. Indeed, the C-set yI=C(I,-) represented by I can be rendered as the free C-set on a single generator of type I. Indeed, we have yI\cong \{ x.f \mid f\in c[I]\} (and we write x\coloneqq x.\mathop{\mathrm{id}}_I), with typing x.f : \textrm{cod}(f) and action (x.f).f' = x.(f; f'). Now it can be made clear through contemplation that for any C-set m, natural transformations yI\Rightarrow m are completely and freely determined by where they send the generator x, so they are in one-to-one correspondence with elements of m of type I.]

Now let us consider the situation where m:\textsf{Poly} is not necessarily constant. In this case, the left action m \to c\mathbin{\triangleleft}m comprises a function on positions and a function on directions. The function on positions, just as before, gives a C-typing and right C-action on the objects of m. The function on directions, given a position P\in m of type I, sends a direction (f:I\to I', p\in m[P.f]) of c\mathbin{\triangleleft}m to a direction in m[P], which we call f.p (as we will see, this is a left action). So now a morphism f:I\to I' not only acts on positions P of type I to produce positions P.f of type I', but it then also acts on directions p\in m[P.f] to produce directions f.p\in m[P]. It is straightfoward (though not necessarily quick) to show that the module axioms tell us: \frac{P:I,\ p\in m[P]}{p.\mathop{\mathrm{id}}_I=p} \qquad \frac{P:I,\ f:I\to I',\ f':I'\to I'',\ p\in m[P.(f; f')]}{f.(f'.p)=(f; f').p} So we see that this is a left action. All in all, we have a functor C\to\textsf{Poly} sending I to \Sigma_{\{P\in m(1)\mid P:I\}}\mathcal{y}^{m[P]} and sending f:I\to I' to the polynomial morphism given by the right and left actions of f. It is of note that we have given a functor C\to\textsf{Poly} a combinatorial description that is just as nice as that of a C-set.

Now we incorporate the right comonoid action m\to m\mathbin{\triangleleft}d. What does this do? The morphism on positions sends P\in m(1) to a pair (P'\in m(1), J_P:m[P']\to d(1)). However, considering the unit law for comodules just on positions shows us that we must have P'=P. So morphism on positions must send P\in m(1) to a pair (P\in m(1), J_P:m[P]\to d(1)). We consider the second element of this pair to be a typing of directions in m[P] by objects of D, and we write (p\in m[P]:(J\in c(1)) to indicate that J_P(p)=J. The morphism on directions, given P\in m(1), sends a direction ((p:J), g:J\to J') of m\mathbin{\triangleleft}d to a direction in m[P], which we call p.g. The right module axioms can be shown to tell us that: \frac{p:J,\ g:J\to J'}{p.g:J'} \qquad \frac{p:J}{p.\mathop{\mathrm{id}}_J=p} \qquad \frac{p:J,\ g:J\to J',\ g':J'\to J''}{(p.g).g'=p.(g; g')} So we see that each direction set m[P] has been upgraded to a D-set.

Now the positions of m have a C-typing and a right action of C, and the directions of m have a D-typing, a right action of D, and a left action of C. This is all the data of a c,d-bicomodule. All that is left is to understand the compatibility condition between the left and right comonoid actions on m. This can be shown to tell us: \frac{P\in m(1),\ f:I\to I',\ (p\in m[P.f]):J}{f.p:J} \tag{$\circledast$} and \frac{P\in m(1),\ f:I\to I',\ (p\in m[P.f]):J,\ g:J\to J'}{f.(p.g)=(f.p).g} \tag{$\circledast$} Thus we have not just a functor C\to\textsf{Poly}, but a functor C to the category \textsf{Set}[D], which is defined as follows. Objects of \textsf{Set}[D] are polynomials p=\Sigma_{I\in p(1)}\mathcal{y}^{p[I]} such that each p[I] is given a D-set structure (i.e. it is the category of elements of a D-set). Morphisms of \textsf{Set}[D] are polynomial morphisms such that the direction maps are D-set homomorphisms, i.e. natural transformations. The conditions (\circledast) tell us exactly this, that the direction maps preserve D-typing and D-action, so they must be D-set homomorphisms.

Now we have a complete picture of bicomodules, suitable for imagining. We can imagine the bicomodule m as a set of positions, each with directions coming out of it. Then C types and acts on the positions covariantly while acting on the directions contravariantly, while D types and acts covariantly on the directions in a compatible way.

4 Implementation

This combinatorial description also lends itself to implementation. In fact, for fixed comonoids c and d (i.e. categories C and D), bicomodules from c to d are models of the following essentially algebraic theory:

Sorts

P_I, the positions of type I, for each I\in c(1).
D_{IJ}, the directions of type J which are over positions of type I, for each I\in c(1) and J\in d(1).

Total Operations

\pi_{IJ}:D_{IJ}\to P_I, for each I\in c(1) and J\in d(1).
f^\flat:P_I\to P_{I'} for each f:I\to I' in C.
g_I:D_{IJ}\to D_{IJ'} for each g:J\to J' in D and each I\in d(1).

Partial Operation

f^\sharp_J:P_I\times D_{I'J}\to D_{IJ} for each f:I\to I' in C and J\in d(1). This operation is defined on a pair (p,d') iff f(p)=\pi_{I'J}(d'). (This condition can also be represented by a pullback.)

Equations

f^\flat; f'^\flat=(f; f')^\flat for all I\xrightarrow{f}I'\xrightarrow{f'}I'' in C.
\mathop{\mathrm{id}}_I^\flat=\mathop{\mathrm{id}}_{P_I} for all I\in c(1).
g_I;\pi_{IJ}=\pi_{IJ'} for all g:J\to J' in D and each I\in d(1).
g_I; g'_I=(g; g')_I for all J\xrightarrow{g}J'\xrightarrow{g'}J'' in D and I\in d(1).
(\mathop{\mathrm{id}}_J)_I=\mathop{\mathrm{id}}_{D_{IJ}} for all I\in c(1) and J\in d(1).
\pi_{IJ}(f_J^\sharp(p,d'))=p for all f:I\to I' in C, J\in d(1), and (p,d')\in P_I\times D_{I'J} on which f_J^\sharp is defined.
For all I\xrightarrow{f}I'\xrightarrow{f'}I'' in C, J\in d(1), and (p,d'')\in P_I\times D_{I''J} on which (f; f')_J^\sharp is defined, (f; f')_J^\sharp(p,d'')=f_J^\sharp(p, {f'}_J^\sharp(f^\flat(p),d'')). (Notice that both sides of this equality are always defined, given the previous rule. This is the nothing but the rule for composition of polynomial morphisms.)
(\mathop{\mathrm{id}}_I)_J^\sharp(p,d)=d for all I\in c(1),J\in d(1), and (p,d)\in P_I\times D_{IJ} on which (\mathop{\mathrm{id}}_I)_J^\sharp is defined.
g_I(f_J^\sharp(p,d'))=f_{J'}^\sharp(p g_{I'}(d')) for all f:I\to I' in C, g:J\to J' in D, and (p,d')\in P_I\times D_{I'J} on which f_J^\sharp is defined.

5 Data migration

Now, we discuss how a bicomodule can be used for data migration. As we have seen, a D-set, i.e. a database with schema D is nothing but a constant left comodule of d. To streamline notation, we notice that this is equivalent to a (d,0)-bicomodule, as a right action by the comonoid 0 forces the polynomial to be constant, since its directions are typed by the positions of the polynomial 0. So given a database d\triangleleft\!\!\overset{X}{\sout{\,\,\phantom{X}\,\,}}\!\!\triangleleft 0, we migrate it to the schema c via the bicomodule c\triangleleft\!\!\overset{m}{\sout{\,\,\phantom{m}\,\,}}\!\!\triangleleft d by means of composition to obtain the bicomodule c\triangleleft\!\!\overset{m\mathbin{\triangleleft}_d X}{\sout{\,\,\phantom{m\mathbin{\triangleleft}_d X}\,\,}}\!\!\triangleleft 0. But what is the nature of this composition? We answer this question first in this case, before giving the general case. First we give the set m\mathbin{\triangleleft}_d X, which is a subset of m(X)=\Sigma_{P\in m(1)}X^{m[P]} (the polynomial m applied to the set X), and then we give the C-typing and action, which make it into a C-set. We give the results here without proof.

m\mathbin{\triangleleft}_d X = \{(P,x)\in m(X) \mid \forall p\in m[P].\ \exists J\in d(1).\ p:J\wedge x(p):J\ \}

So the composite m\mathbin{\triangleleft}_d X is obtained from m(X) by filtering for elements on which the map x respects the D-typings on m and X. The C-typing on m\mathbin{\triangleleft}_d X is defined straightforwardly: whenever P:I we have (P,x):I. And the C-action is defined by (P,x).f\coloneqq (P.f, (p'\mapsto x(f.p'))). All this would not be hard to implement. Yet such a data transformation is extremely general, encompassing all “FQL queries” as described in Relational Foundations for Data Migration (albeit with no attributes).

Finally, we describe the composition of two bicomodules c\triangleleft\!\!\overset{m}{\sout{\,\,\phantom{m}\,\,}}\!\!\triangleleft d and d\triangleleft\!\!\overset{n}{\sout{\,\,\phantom{n}\,\,}}\!\!\triangleleft e. This composition m\mathbin{\triangleleft}_d n is obtained from the polynomial m\mathbin{\triangleleft}n by taking a subset of positions, and then for each of those positions, a quotient of directions. \begin{aligned} m\mathbin{\triangleleft}_d n(1) &= \{(P,Q)\in m\mathbin{\triangleleft}n(1) \mid \forall p\in m[P].\ \exists J\in d(1).\ p:J\wedge Qp:J\ \} \\ m\mathbin{\triangleleft}_d n[(P,Q)] &= m\mathbin{\triangleleft}n[(P,Q)] / \sim_{PQ} \textrm{ where $\sim_{PQ}$ is generated by }\\ &\quad\frac{g:J\to J'\textrm{ in }D}{(p.g,q)\sim (p,g.q)} \end{aligned} Again the filter on positions expresses the agreement between the D-typings on m and n, while now we also have a quotient on directions expressing the agreement between the D-actions on m and n, in a manner reminiscent of the definition of tensor of bimodules in linear algebra. The C-typing and action on positions are defined similarly as in the e=0 case: P:I\Rightarrow (P,Q):I and (P,Q).f\coloneqq (P.f, (p'\mapsto Q(f.p'))). We now have also a left C-action on directions, defined by f.(p',q)=(f.p',q) and a right E-action on directions, defined by (p,q).h = (p,q.h).

6 Conclusion

I hope that the above helps people imagine and implement bicomodules, their composition, and their application to data migration. Let me know how you fare in imagining and implementing these things.