Retrotransformations
This post is cross-posted at the Topos Institute blog.
In recent work, Michael Lambert and I showed that cartesian double theories and their models, which are span-valued cartesian lax functors, provide a unifying framework for doctrines, at least up to a certain level in the hierarchy of categorical logic (Lambert and Patterson 2024). We considered two kinds of morphisms between lax double functors, namely lax natural transformations1 and modules, and showed that they form the arrows and proarrows of a (virtual) double category. Yet there is a third known kind of morphism between lax functors, transformations whose components are proarrows rather than arrows. We did not consider such “protransformations” between models of double theories. Are they good for anything? The answer, it turns out, is yes!
In this post, we will see that lax protransformations of a special kind, which I call “retrotransformations” after Robert Paré’s “retrocells” (Paré 2023), generalize a concept that has attracted interest lately: cofunctors. A cofunctor between categories is the purest distillation of the bidirectional mapping that occurs in a split opfibration or a delta lens, where objects are sent “forward” and morphisms are sent “backward” in a compatible way. The inspiration for this post is Bryce Clarke’s PhD thesis, The double category of lenses (Clarke 2022b), where cofunctors are shown to be the “retromorphisms” arising from retrocells in a double category. Alternatively, cofunctors are morphisms between polynomial comonoids, a point of view thoroughly investigated by my colleagues at Topos Institute (Niu and Spivak 2023).
The big picture is that retrotransformations fit into this table:
| Single object | Multi-object |
|---|---|
| Functor | Natural transformation |
| Cofunctor | Retrotransformation |
| Profunctor | Module |
The left column lists notions of morphism between categories. The right column lists notions of morphism between lax functors \(F, G: \mathbb{D} \to \mathbb{E}\), which when specialized to lax functors \(F, G: \mathbb{1} \to \mathbb{S}\mathsf{pan}\) recover the left column. Thus, a retrotransformation is a “multi-object cofunctor” or, more generally, a “multi-object retromorphism.”
Retrotransformations between models of double theories are a device for generating new kinds of “generalized cofunctors,” which seems especially useful since cofunctors are so much less studied than functors or profunctors. As illustrations, we define “monoidal cofunctors” between monoidal categories and “multicofunctors” between multicategories. Analogously, we can define delta lenses between monoidal categories and between multicategories.
Lax protransformations
As usual with such matters, protransformations have a slick, conceptual definition, which then needs to be unpacked to be useful in any concrete situation. Let’s start with the conceptual definition.
Definition 1 Let \(F,G: \mathbb{D} \to \mathbb{E}\) be lax functors between double categories, viewed as pseudocategories in \(\mathbf{Cat}\). A lax protransformation \(\tau: F \mathrel{\mkern 3mu\vcenter{\hbox{$\scriptstyle\mid$}}\mkern-8mu{\Rightarrow}}G\) is a lax natural transformation from \(F\) to \(G\), internal to \(\mathbf{Cat}\).
So, a lax protransformation \(\tau: F \mathrel{\mkern 3mu\vcenter{\hbox{$\scriptstyle\mid$}}\mkern-8mu{\Rightarrow}}G\) consists of first, a functor \(\tau_0: \mathbb{D}_0 \to \mathbb{E}_1\), the components of the protransformation, which must well-typed in that the diagram
commutes; and second, a natural transformation
giving the pronaturality comparisons of the lax protransformation, which must also be well-typed in that the pasting below involving the source functor
is equal to the identity on \(F_0 \circ s = s \circ F_1: \mathbb{D}_1 \to \mathbb{E}_0\), and similarly for the target functor. That is to say, the source and target of each component of \(\tau_1\) are identity arrows. Finally, the naturality comparisons must be coherent with respect to external composition and identities. We omit these final two commutative diagrams, but they can be found in (Martins-Ferreira 2006, Equations 3.5 & 3.6).
We are halfway done unpacking the definition. When it is fully unpacked, we recover a definition mildly generalizing that in (Grandis 2019, Definition 3.8.2). With the abbreviations \(\tau_x \coloneqq \tau_0(x)\), \(\tau_f \coloneqq \tau_0(f)\), and \(\tau_m \coloneqq (\tau_1)_m\) for objects \(x\), arrows \(f\), and proarrows \(m\) in \(\mathbb{D}\), a lax protransformation \(\tau: F \mathrel{\mkern 3mu\vcenter{\hbox{$\scriptstyle\mid$}}\mkern-8mu{\Rightarrow}}G: \mathbb{D} \to \mathbb{E}\) is seen to consist of
for each object \(x \in \mathbb{D}\), a proarrow \(\tau_x: Fx \mathrel{\mkern 3mu\vcenter{\hbox{$\shortmid$}}\mkern-10mu{\to}}Gx\) in \(\mathbb{E}\), the component of \(\tau\) at \(x\);
for each arrow \(f: x \to y\) in \(\mathbb{D}\), a cell \(\tau_f\) in \(\mathbb{E}\) of the form
called the component of \(\tau\) at \(f\);
for each proarrow \(m: x \mathrel{\mkern 3mu\vcenter{\hbox{$\shortmid$}}\mkern-10mu{\to}}y\) in \(\mathbb{D}\), a globular cell \(\tau_m\) in \(\mathbb{E}\) of the form
called the pronaturality comparison of \(\tau\) at \(m\).
These must satisfy the following axioms.
Functorality of components: \(\tau_{f \cdot g} = \tau_f \cdot \tau_g\) and \(\tau_{1_x} = 1_{\tau_x}\).
Naturality with respect to cells: for every cell \(\alpha: m \to n\) in \(\mathbb{D}\) with source \(f\) and target \(g\),
Coherence with respect to external composition: for every pair of composable proarrows \(m: x \mathrel{\mkern 3mu\vcenter{\hbox{$\shortmid$}}\mkern-10mu{\to}}y\) and \(n: y \mathrel{\mkern 3mu\vcenter{\hbox{$\shortmid$}}\mkern-10mu{\to}}z\) in \(\mathbb{D}\),
Coherence with respect to external identities: for every object \(x \in \mathbb{D}\),
Finally, we say that a lax protransformation \(\tau\) is pseudo if \(\tau_1\) is a natural isomorphism, i.e., each comparison cell \(\tau_m\) is invertible. This definition of a pseudo protransformation agrees with (Grandis 2019, Definition 3.8.2).2
It is interesting to ask what lax protransformations look like in examples, but we will set this aside for now and turn immediately to a specialization of the concept.
Retrotransformations
We are interested in lax protransformations whose components at objects, despite being proarrows, are obtained from ordinary arrows. That is what companions in a double category do. A companion of an arrow \(f: x \to y\) is a proarrow \(f_!: x \mathrel{\mkern 3mu\vcenter{\hbox{$\shortmid$}}\mkern-10mu{\to}}y\) along with two cells that bind \(f\) and \(f_!\) together in a suitable way. For a review of companions, see (Paré 2023, sec. 1). A double category with companions and conjoints is precisely an equipment (Shulman 2008, Theorem 4.1), but merely having companions is enough for present purposes.
A retrotransformation between lax functors is a lax protransformation whose components at objects are companions, in a coherent way.
Definition 2 Let \(\mathbb{D}\) and \(\mathbb{E}\) be double categories, where \(\mathbb{E}\) has companions, and let \(F,G: \mathbb{D} \to \mathbb{E}\) be lax functors. A retrotransformation \((\phi, \tau): F \mathrel{\mkern 3mu\vcenter{\hbox{$\scriptstyle\mid$}}\mkern-8mu{\Rightarrow}}G\) consists of
- a natural transformation \(\phi: F_0 \Rightarrow G_0\) between functors, and
- a lax protransformation \(\tau: F \mathrel{\mkern 3mu\vcenter{\hbox{$\scriptstyle\mid$}}\mkern-8mu{\Rightarrow}}G\) between lax functors
such that
- for every object \(x\) in \(\mathbb{D}\), the proarrow \(\tau_x = (\phi_x)_!: Fx \mathrel{\mkern 3mu\vcenter{\hbox{$\shortmid$}}\mkern-10mu{\to}}Gx\) in \(\mathbb{E}\) is the companion of the arrow \(\phi_x: Fx \to Gx\), and
- for every arrow \(f: x \to y\), the cell \(\tau_f\) is induced by the naturality square for \(\phi\) at \(f\).
Let us clarify the meaning of the last condition. By the sliding rule for companions (Paré 2023, sec. 1), the component of a retrotransformation at an arrow \(f: x \to y\)
can be identified with a special cell
The last condition in the definition of a retrotransformation says that the cell \(\bar\tau_f\) is the image under the external identity \(\operatorname{id}: \mathbb{E}_0 \to \mathbb{E}_1\) of the naturality square
So, contrary to initial appearances, a retrotransformation actually contains less data than a general lax protransformation. There is, for each object \(x \in \mathbb{D}\), the component \(\phi_x: Fx \to Gx\), and for each proarrow \(m: x \mathrel{\mkern 3mu\vcenter{\hbox{$\shortmid$}}\mkern-10mu{\to}}y\) in \(\mathbb{D}\), the pronaturality comparison
The sliding rule cannot be used to simplify these cells, which are what give retrotransformations their distinctive character.
The following proposition explains how a retrotransformation between lax functors is a “multi-object retromorphism” in the sense of Paré (2023). Recall that if \(\mathbb{D}\) is a strict double category and \(F: \mathbb{D} \to \mathbb{S}\mathsf{pan}\) is a lax functor, then each set \(Fx\) in the image of \(F\) becomes the set of objects of a category. To say this more generally and precisely, for any double category \(\mathbb{E}\), a lax functor \(F: \mathbb{D} \to \mathbb{E}\) sends each object \(x\) in \(\mathbb{D}\) to a category object3 \((Fx, F\operatorname{id}_x, F_{x,x}, F_x)\) in \(\mathbb{E}\). For more details, see (Lambert and Patterson 2024, sec. 2).
Proposition 1 Let \(F,G: \mathbb{D} \to \mathbb{E}\) be lax functors from a strict double category \(\mathbb{D}\) to a double category \(\mathbb{E}\) with companions, and let \((\phi, \tau): F \mathrel{\mkern 3mu\vcenter{\hbox{$\scriptstyle\mid$}}\mkern-8mu{\Rightarrow}}G\) be a retrotransformation. Then for each object \(x\) in \(\mathbb{D}\), the pair \((\phi_x, \tau_{\operatorname{id}_x})\) is a retromorphism from the category \((Fx, F\operatorname{id}_x, F_{x,x}, F_x)\) to the category \((Gx, G\operatorname{id}_x, G_{x,x}, G_x)\) in \(\mathbb{E}\). In particular, when \(\mathbb{E}\) is \(\mathbb{S}\mathsf{pan}\), the pair \((\phi_x, \tau_{\operatorname{id}_x})\) is a cofunctor between categories.
Proof. For each object \(x \in \mathbb{D}\), the component \(\phi_x: Fx \to Gx\) is the arrow part of a retromorphism and the comparison cell
is the retrocell part of the retromorphism. The two coherence axioms for a lax protransformation immediately give the two axioms of a retromorphism (Paré 2023, Definition 6.1). The last statement follows because retromorphisms between categories (in \(\mathbb{S}\mathsf{pan}\)) are known to be cofunctors (Paré 2023, Example 6.7). \(\square\)
Corollary 1 A retrotransformation between lax functors \(\mathbb{1} \to \mathbb{S}\mathsf{pan}\) is precisely a cofunctor between categories.
Delta lenses between lax functors
The description of a delta lens as a compatible pairing of a functor with a cofunctor (Clarke 2020) suggests that a delta lens between lax functors should be defined as a compatible pairing of a natural transformation with a retrotransformation.
Definition 3 Let \(\mathbb{D}\) and \(\mathbb{E}\) be double categories, where \(\mathbb{E}\) has companions, and let \(F,G: \mathbb{D} \to \mathbb{E}\) be lax functors. A delta lens \((\phi, \tau)\) from \(F\) to \(G\) is a (strict) natural transformation \(\phi: F \Rightarrow G\) together with a lax protransformation \(\tau: F \mathrel{\mkern 3mu\vcenter{\hbox{$\scriptstyle\mid$}}\mkern-8mu{\Rightarrow}}G\), satisfying the following two compatibility axioms.
- Compatibility on objects: the pair \((\phi_0, \tau)\) is a retrotransformation, where \(\phi_0: F_0 \Rightarrow G_0\) denotes the ordinary natural transformation underlying \(\phi\).
- Compatibility on proarrows: for every proarrow \(m: x \mathrel{\mkern 3mu\vcenter{\hbox{$\shortmid$}}\mkern-10mu{\to}}y\) in \(\mathbb{D}\), we have
The second axiom says that the cell \(\tau_m\) is a section of \(\phi_m\), modulo the binding cells for the companions (denoted by square brackets).
Proposition 2 Let \(F,G: \mathbb{D} \to \mathbb{E}\) be lax functors from a strict double category \(\mathbb{D}\) to a double category \(\mathbb{E}\) with companions, and let \((\phi, \tau)\) be a delta lens from \(F\) to \(G\). Then for each object \(x\) in \(\mathbb{D}\), the pairs \((\phi_x, \phi_{\operatorname{id}_x})\) and \((\phi_x, \tau_{\operatorname{id}_x})\) form a lens from the category \((Fx, F\operatorname{id}_x, F_{x,x}, F_x)\) to the category \((Gx, G\operatorname{id}_x, G_{x,x}, G_x)\) in \(\mathbb{E}\).
Proof. The pair \((\phi_x, \phi_{\operatorname{id}_x})\) is a functor, whereas \((\phi_x, \tau_{\operatorname{id}_x})\) is a cofunctor/retromorphism by the previous proposition. That these are suitably compatible also follows directly. Specifically, Clarke (2022b) defines a delta lens between category objects abstractly, but gives a concrete description in (Clarke 2022b, Equation 5.19). That equation is precisely the second compatibility axiom above, instantiated at the proarrow \(\operatorname{id}_x: x \mathrel{\mkern 3mu\vcenter{\hbox{$\shortmid$}}\mkern-10mu{\to}}x\). \(\square\)
Corollary 2 A delta lens between lax functors \(\mathbb{1} \to \mathbb{S}\mathsf{pan}\) is precisely a delta lens between categories.
Cartesian lax protransformations
In order to study generalized cofunctors between categorical structures such as monoidal categories and multicategories, we must consider models of cartesian double theories and lax protransformations between such models. One way to define a cartesian double category is as a pseudocategory in \(\mathbf{CartCat}\), the 2-category of categories with finite products, functors preserving finite products, and natural transformations.4 This immediately suggests the following definition.
Definition 4 Let \(F,G: \mathbb{D} \to \mathbb{E}\) be cartesian lax functors between cartesian double categories, viewed as pseudocategories in \(\mathbf{CartCat}\). A cartesian lax protransformation is lax natural transformation from \(F\) to \(G\), internal to \(\mathbf{CartCat}\).
Equivalently, a lax protransformation \(\tau: F \mathrel{\mkern 3mu\vcenter{\hbox{$\scriptstyle\mid$}}\mkern-8mu{\Rightarrow}}G\) between cartesian lax functors is cartesian if the underlying functor \(\tau_0: \mathbb{D}_0 \to \mathbb{E}_1\) preserves finite products, i.e., there are canonical isomorphisms \(\tau_{x \times x'} \cong \tau_x \times \tau_{x'}\) and \(\tau_{1_{\mathbb{D}_0}} \cong 1_{\mathbb{E}_1}\).
No extra conditions are needed for a retrotransformation or delta lens \((\phi, \tau)\) between cartesian lax functors. Since natural transformations and companions both preserve products, the assignment \(\tau_x = (\phi_x)_!\) is always product-preserving.
Example: monoidal cofunctors between monoidal categories
To my knowledge, no notion of structure-preserving cofunctor between monoidal categories has been defined in the literature. We give a definition using the machinery developed so far. Let \(\mathbb{T}_{\mathsf{PsMon}}\) be the cartesian double theory of pseudomonoids (Lambert and Patterson 2024, Theory 6.6), whose models are (weak) monoidal categories.
Definition 5 A monoidal cofunctor (resp. monoidal delta lens) between monoidal categories is a retrotransformation (resp. delta lens) between the corresponding cartesian lax functors \(\mathbb{T}_{\mathsf{PsMon}} \to \mathbb{S}\mathsf{pan}\).
Let’s sketch what a monoidal cofunctor amounts to concretely. Let \((\phi, \tau): F \mathrel{\mkern 3mu\vcenter{\hbox{$\scriptstyle\mid$}}\mkern-8mu{\Rightarrow}}G\) be a retrotransformation between models \(F,G: \mathbb{T}_{\mathsf{PsMon}} \to \mathbb{S}\mathsf{pan}\), regarded as monoidal categories. The generating object \(x\) of \(\mathbb{T}_{\mathsf{PsMon}}\) yields a cofunctor \((\phi_x, \tau_{\operatorname{id}_x})\) between the underlying categories of the monoidal categories. By naturality with respect to the arrows \(\otimes: x^2 \to x\) and \(I: 1 \to x\) in \(\mathbb{T}_{\mathsf{PsMon}}\), the diagrams
commute, i.e., the object map of the cofunctor strictly preserves the monoidal product and unit. Next, naturality with respect to the cells \(\operatorname{id}_\otimes: \operatorname{id}_x^2 \to \operatorname{id}_x\) and \(\operatorname{id}_I: 1 \to \operatorname{id}_x\) says that the morphism map of the cofunctor preserves the monoidal product and unit. For example, the first of the two equations is
The equation is well-typed (i.e., the cell \(\tau_\otimes\) exists) by the above naturality square for \(\otimes: x^2 \to x\), and it says that the monoidal product of the liftings of a pair of morphisms is equal to the lifting of the monoidal product. Finally, naturality with respect to the associator and unitor cells in the double theory say that liftings of morphisms preserve associators and unitors in the monoidal categories.
Thus, a monoidal delta lens from a monoidal category \(\mathsf{C}\) to another \(\mathsf{D}\) is a strict monoidal functor \(\mathsf{C} \to \mathsf{D}\) together with a monoidal cofunctor \(\mathsf{C} \mathrel{\mkern 3mu\vcenter{\hbox{$\shortmid$}}\mkern-10mu{\to}}\mathsf{D}\), which share an object map and have the property that the cofunctor’s lifting operation is a section of the functor’s morphism map.
It may seem strange that monoidal cofunctors and monoidal delta lenses strictly preserve monoidal products, even for weak monoidal categories, but this is consistent with related ideas in the literature. Shulman defines a monoidal opfibration between monoidal categories to be a functor that is both an opfibration and a strict monoidal functor, such that the monoidal product of the domain category preserves opcartesian liftings (Shulman 2008, sec. 12). A monoidal delta lens is what remains of a split monoidal opfibration when the universal property is discarded, just as a delta lens is for a split opfibration.
Example: multicofunctors between multicategories
Although often regarded as obscure, multicategories are in many ways simpler than monoidal categories, and the same is true for multicofunctors compared with monoidal cofunctors. Let \(\mathbb{T}_{\mathsf{Promon}}\) be the cartesian double theory of promonoids (Lambert and Patterson 2024, Theory 6.8), whose (lax) models are multicategories. In this theory, there is a unique proarrow of form \(p_n: x^n \mathrel{\mkern 3mu\vcenter{\hbox{$\shortmid$}}\mkern-10mu{\to}}n\) for every arity \(n \geq 0\), whose image in a model is the span of \(n\)-ary multimorphisms.
Definition 6 A multicofunctor5 (resp. delta lens) between multicategories is a retrotransformation (resp. delta lens) between the corresponding cartesian lax functors \(\mathbb{T}_{\mathsf{Promon}} \to \mathbb{S}\mathsf{pan}\).
Let’s take a quick look at a retrotransformation \((\phi, \tau): F \mathrel{\mkern 3mu\vcenter{\hbox{$\scriptstyle\mid$}}\mkern-8mu{\Rightarrow}}G\), identifying the models \(F,G: \mathbb{T}_{\mathsf{Promon}} \to \mathbb{S}\mathsf{pan}\) with multicategories \(\mathcal{M}\) and \(\mathcal{N}\). The data consists of the component \(\phi_x: Fx \to Gx\), giving a map between objects \(f: \operatorname{Ob}\mathcal{M} \to \operatorname{Ob}\mathcal{N}\), and for each arity \(n \geq 0\), the pronaturality comparison
giving a lifting operation \(\tau_n \coloneqq \tau_{p_n}\) on \(n\)-ary multimorphisms, which can be pictured as
Because the theory of promonoids has no nontrivial arrows or cells, the only relevant axioms are the coherence axioms for lax protransformations. These axioms say that the lifting operations preserve composition of multimorphisms and identity morphisms in the multicategories.
Discussion
In a sense, this post completes the story about morphisms between models of cartesian double theories begun in (Lambert and Patterson 2024). There are three more-or-less known notions of morphism between lax double functor—natural transformations, protransformations, and modules—and they have all been shown to give useful notions of morphism between models, generalizing functors, cofunctors, and profunctors between categories.
There is plenty more that remains to be said. For starters, functors and cofunctors between categories form a double category (Clarke 2022b, sec. 3.1) and so should natural transformations and retrotransformations between lax double functors. There is a known notion of modification between natural transformations and pseudo protransformations (Grandis 2019, Definition 3.8.3) that could be plausibly be adapted to this purpose. However, the details need to be worked out. Beyond that, it is natural to wonder how all three notions of morphism between lax functors fit together and whether they can be united inside some three-dimensional structure.
References
Footnotes
Our usage of “natural transformation” follows Paré (2011). Under our orientation convention, where arrows are vertical and proarrows are horizontal, natural transformations are also called “vertical transformations.” However, the meaning of the latter phrase varies from author to author, hence our desire to avoid it.↩︎
Besides using different terminology for pseudo protransformations, Grandis takes his comparison cells to go in the oplax, rather than the lax, direction. Of course, this makes no difference in the pseudo case.↩︎
Terminology for categories internal to a double category varies. Paré (2023) calls them “monads,” which is meant to evoke “monads in the underlying bicategory of the double category.”↩︎
Recall that such a natural transformation automatically preserves finite products in the sense that it is a monoidal natural transformation for any choice of cartesian monoidal structure.↩︎
A different but equivalent definition of a multicofunctor is as a retromorphism between category objects in the double category of \(T\)-spans, where \(T = \operatorname{List}\) is the list monad (Clarke 2022a, 14). Thanks to Bryce Clarke for pointing this out.↩︎