Retrotransformations
category theory
categorical logic
double categories
lenses
Abstract
Retrotransformations between lax double functors are introduced as the “multi-object” analogue of a cofunctor between categories. Notions of “monoidal cofunctor” between monoidal categories and of “multicofunctor” between multicategories are then derived as special cases.
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 2023). 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.
1 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.
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{$\scriptstyle+$}}\mkern-12mu{\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{$\scriptstyle+$}}\mkern-12mu{\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{$\scriptstyle+$}}\mkern-12mu{\to}}y and n: y \mathrel{\mkern 3mu\vcenter{\hbox{$\scriptstyle+$}}\mkern-12mu{\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.
2 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{$\scriptstyle+$}}\mkern-12mu{\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.
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{$\scriptstyle+$}}\mkern-12mu{\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 2023, sec. 2).
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
3 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
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{$\scriptstyle+$}}\mkern-12mu{\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).
Proof. 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{$\scriptstyle+$}}\mkern-12mu{\to}}x.
4 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.
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.
5 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 2023, Theory 6.6), whose models are (weak) monoidal categories.
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{$\scriptstyle+$}}\mkern-12mu{\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.
6 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 2023, 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{$\scriptstyle+$}}\mkern-12mu{\to}}n for every arity n \geq 0, whose image in a model is the span of n-ary multimorphisms.
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.
7 Discussion
In a sense, this post completes the story about morphisms between models of cartesian double theories begun in (Lambert and Patterson 2023). 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
Clarke, Bryce. 2020. “Internal Split Opfibrations and Cofunctors.” Theory and Applications of Categories 35 (44): 1608–33. http://www.tac.mta.ca/tac/volumes/35/44/35-44abs.html.
———. 2022a. “A General Framework for Cofunctors.” Presented at the Computer science theory seminar, Tallinn University of Technology. https://bryceclarke.github.io/talk-slides/2022-04-Computer-science-theory-seminar.pdf.
———. 2022b. “The Double Category of Lenses.” PhD thesis, Macquarie University. https://figshare.mq.edu.au/articles/thesis/22045073.
Grandis, Marco. 2019. Higher Dimensional Categories: From Double to Multiple Categories. World Scientific. https://doi.org/10.1142/11406.
Lambert, Michael, and Evan Patterson. 2023. “Cartesian Double Theories: A Double-Categorical Framework for Categorical Doctrines.” https://arxiv.org/abs/2310.05384.
Martins-Ferreira, Nelson. 2006. “Pseudo-Categories.” Journal of Homotopy and Related Structures 1 (1): 47–78. https://arxiv.org/abs/math/0604549.
Niu, Nelson, and David Spivak. 2023. Polynomial Functors: A Mathematical Theory of Interaction. https://github.com/ToposInstitute/poly.
Paré, Robert. 2011. “Yoneda Theory for Double Categories.” Theory and Applications of Categories 25 (17): 436–89. http://www.tac.mta.ca/tac/volumes/25/17/25-17abs.html.
———. 2023. “Retrocells.” https://arxiv.org/abs/2306.06436.
Shulman, Michael. 2008. “Framed Bicategories and Monoidal Fibrations.” Theory and Applications of Categories 20 (18): 650–738. http://www.tac.mta.ca/tac/volumes/20/18/20-18abs.html.
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.↩︎