Which direction does a lax dinatural transformation go?

Question

In 2-category theory we often encounter notions with noninvertible coherence 2-cells, in which case there is a choice about which way the 2-cell should point. Generally, one of these directions is called "lax" and the other "colax" (or "oplax"). We have to make at least one arbitrary choice for which of the two to call "lax" and which to call "colax", but once we've made that choice in one place, the choices everywhere else are determined. One general place to phrase the choice is as defining lax and colax morphisms of algebras for a 2-monad; everything else can be seen as either an instance of that or a generalization of that, and that tells you which direction is lax and which is colax (at least if you want to be consistent, which not everyone does).

At least, that's what I used to think. But today I started thinking about lax dinatural transformations, which should be like ordinary dinatural transformations but with a 2-cell inhabiting the dinaturality hexagon. There are two directions that that 2-cell can go in, but I can't figure out a way to relate those directions to any other situation that has a lax and a colax version.

Since dinatural transformations don't even compose in general, there's no clear way to see them as morphisms of algebras for some monad. The obvious thing to do would be to specialize a dinatural transformation to a natural one by making the two functors either both totally covariant or both totally contravariant, and then compare to the usual terminology in that special case. But there are two ways to do this (covariant or contravariant), and the same direction of 2-cell in a dinaturality hexagon specializes to a lax natural transformation in one case and a colax one in the other case. I suppose we could choose to name it according to the covariant direction because "covariant functors are more basic than contravariant ones", but that feels more arbitrary than I'd like.

You can also specialize a dinatural transformation to an extranatural transformation. But I've looked at the references cited here about lax extranatural transformations, and as far as I can see none of them gives any reason for choosing which direction is lax and which is colax.

It is, of course, true that if you change the domain category to its opposite, permuting the domain to regard a functor $F:C^{\rm op}\times C\to D$ as a functor $F:(C^{\rm op})^{\rm op}\times C^{\rm op}\to D$, then the direction of the 2-cell in a dinaturality hexagon switches. This is not the case for ordinary natural transformations, and suggests that maybe there is more arbitrariness in the dinatural and extranatural case than in the ordinary one.

But I still have to ask, in case anyone else can see something I can't: Is there any principled way to decide which direction of a 2-cell in a dinaturality hexagon (or an extranaturality wedge) is "lax" and which is "colax"?

Answer 1

This is a very loose answer since it's based on something that, as far as I know, has not been fully formalized. The key idea is that of what I might call a "dependent arrow" between two objects.

The closest analogy is to that of a dependent path in HoTT, where if we have $a, a' : A$, $p : a = a'$, $b : B(a)$ and $b' : B(a')$, then even though $b$ and $b'$ have different types, we can still talk about paths between them using $p$. Specifically, the type of dependent paths is $p \# b = b'$, where $\#$ denotes transportation. As you probably, know, if $f : \Pi_{a : A} B(a)$, then $f$ maps a path $p : a = a'$ to a dependent path $apD_f(p) : p \# f(a) = f(a')$.

In a hypothetical directed (homotopy) type theory, we might have the same information, but with $p$ replaced with a directed morphism from $a$ to $a'$ and $B$ somehow functorial. Now transporting $b$ along $p$ means $B(p)(b)$, where $B(p)$ is the functorial action of $B$ on morphisms in $A$. A dependent arrow from $b$ to $b'$ over $p$ is a morphism $B(p)(b) \to b'$ in $B(a')$.

If $B$ is instead contravariant, then we have to transport $b'$ instead. That's because $B(p) : B(a') \to B(a)$ now, so we can't apply it to $b$ anymore. Thus, a dependent arrow from $b$ to $b'$ over $p$ should be a morphism $b \to B(p)(b')$.

In general, as we'll see below, $B$ might depend both covariantly and contravariantly on $a$, so we have to transport both $b$ and $b'$ to make sense of a morphism between them. Again, I've not seen a formalization of this, so forgive me if it's a bit fuzzy.

We'll denote this type of "dependent arrows over $p$" as $b \to_p b'$.

Let's see how this works with an example. Let $F, G: C \to D$ be functions (functors). If a directed morphism from $F$ to $G$ is to be analogous to a path from $F$ to $G$, one might expect such a morphism to be a pointwise morphism $\alpha_c : F(c) \to G(c)$ for each $c : C$.

What about the action of $\alpha$ on morphisms? For $f : c \to c'$ in $C$, this should be a dependent arrow $\alpha_c \to_f \alpha_{c'}$.

In this case, the type of $\alpha_c : F(c) \to G(c)$ depends on $c$ both covariantly and contravariantly. To get a dependent arrow from $\alpha_c$ to $\alpha_{c'}$ over $f$, we need to transport both sides. For $\alpha_c$, we can post-compose with $G(f)$ and for $\alpha_{c'}$, we can pre-compose with $F(f)$. Thus, a dependent path in this case is a 2-cell $G(f) \circ \alpha_c \Rightarrow \alpha_{c'} \circ F(f)$.

If we're thinking of $D$ as a 1-category, the 2-cells are just identities, so this reduces to naturality. If D is instead a 2-category, then what we get here is a lax natural transformation. If we want an oplax transformation, then what we should do is instead map $f : c \to c'$ to a dependent map $\alpha_{c'} \to_f \alpha_c$.

---

Let's try this out for dinatural transformations. This is where things get (at least for me) very fuzzy. We want to repeat the above, but allow $F$ and $G$ to be both covariant and contravariant at once. I think of $F$ and $G$ has "normally" only having a single variable, but then having a two-variable "extension".

In our hypothetical directed type theory, this sort of thing shows up all the time. For example, the type of $id_c : \hom_C(c, c)$ is not covariant or contravariant, but $\hom_C$ can be extended to a two-variable functor $C^{op} \times C \to Type$, which makes it both covariant and contravariant.

In any case, we can try our best. A morphism from $F$ to $G$ is again pointwise, but rather than $\alpha_{c, c'} : F(c, c') \to G(c, c')$, we want to think of $F$ and $G$ as being single-variable here, to get $\alpha_c : F(c, c) \to G(c, c)$.

The action of $\alpha$ on morphisms takes a morphism $f : c \to c'$ in $C$ to a morphism $\alpha_f : \alpha_c \to_f \alpha_c'$. As in the case of natural transformations, both sides need to be transported. The covariant transport takes $\alpha_c$ to $G(1, f) \circ \alpha_c \circ F(f, 1) : F(c', c) \to G(c, c')$. The contravariant transport takes $\alpha_{c'}$ to $G(f, 1) \circ \alpha_{c'} \circ F(1, f) : F(c', c) \to G(c, c')$. Sketching this out, we get the hexagon for dinaturality.

Thus, if we follow the same convention as with natural transformations, a lax dinatural transformation has a 2-cell $\alpha_c$ to $G(1, f) \circ \alpha_c \circ F(f, 1) \Rightarrow G(f, 1) \circ \alpha_{c'} \circ F(1, f)$ and an oplax dinatural transformation has the reverse direction. The key here is that the lax version maps $f$ to $\alpha_c \to_f \alpha_{c'}$.