The skew monoidal structure induced by a functor

(This is not a proof, but just some thoughts on abstracting the construction which could potentially be helpful for finding a more conceptual proof of the coherence laws. In any case, I find it fun to think along these lines...)

I suggest it might be useful to generalize this construction by considering it in bifibrational terms. To understand this generalization, first let's repackage the original 2-category $\mathcal{K}$ by building the lax slice category $\mathcal{K}⫽B$, whose objects are pairs $(A,x : A \to B)$ and whose morphisms $(A_1,x_1) \to (A_2,x_2)$ are pairs $(f : A_1 \to A_2, \alpha : x_1 \to x_2\circ f)$. Assuming $\mathcal{K}$ has all left kan extensions, then the forgetful functor $\mathcal{K}⫽B \to \mathcal{K}$ is a bifibration. Moreover, it has the special property that the fiber over $B$ (= endomorphisms of $B$) is a monoidal category which acts on every other fiber (via postcomposition), and that this monoidal action commutes with the action of pullback (which is defined via precomposition). These are all the things we need in order to define the skew monoidal structure induced by a 1-cell $j$ in $\mathcal{K}$, which we will now consider more abstractly.

Let us assume given:

1. A bifibration $\mathcal{E} \to \mathcal{B}$ (we write $f_!$ and $f^*$ for the push and pull along any morphism $f$ in $\mathcal{B}$);
2. An object $b \in B$ (the "target") with a monoidal structure $(\circ,i)$ on the fiber category $\mathcal{E}_b$;
3. A monoidal action $$* : \mathcal{E}_b \times \mathcal{E}\to \mathcal{E}$$ which is fiber-preserving, in the sense that it lies over the trivial action $1 \times \mathcal{B} \to \mathcal{B}$, and which restricts to the monoidal product on the fiber over $b$;
4. Finally, observe that by the universal properties of push/pull and the fact that the action $*$ is fiber-preserving, there are canonical maps: \begin{align} f_! (x * y) \to x * f_! y \tag{1} \\ x * f^* y \to f^* (x * y) \tag{2} \end{align} We will assume that (2) is invertible, i.e., that the action preserves cartesian morphisms (but not necessarily opcartesian ones).

Note that all of these axioms are satisfied by the example of $\mathcal{K}⫽B \to \mathcal{K}$ above.

Given any such a structure, I claim that any morphism $j : a \to b$ into the target object induces a skew monoidal structure on the fiber category $\mathcal{E}_a$, where the tensor of two objects $x,y \in \mathcal{E}_a$ is defined by $$x \bullet y := j_! x * y$$ and the unit object is defined by $$I := j^* i.$$

Here is how we build the structure maps:

• [associator $(x \bullet y) \bullet z \to x \bullet (y \bullet z)$] $$ j_!(j_! x * y) * z \to (j_! x \circ j_! y) * z \cong j_! x * (j_! y * z) $$ where we use (1) above, that $*$ restricts to the monoidal product on the fiber over $b$, and that it is a monoidal action.
• [left unitor $I \bullet x \to x$] $$ j_! (j^* i) * x \to i * x \cong x $$ where we use the counit of the push-pull adjunction and that $i$ is a unit for the monoidal action.
• [right unitor $x \to x \bullet I$] $$ x \to j^* j_! x \cong j^* (j_! x \circ i) \to j_! x * j^* i $$ where we use the unit of the push-pull adjunction, that $i$ a right unit for the monoidal product, and the inverse to (2) above.

Now of course we have to check the five coherence laws! I haven't done that, but I suspect it will be more fun than in the original setting of $\mathcal{K}$. What do you think?

For the case $\mathcal{K} = \mathbf{Cat}$, there is indeed a worked out proof that this structure on the functor category $[A,B]$ (given by the tensor product $x \bullet y := j_! x \circ y$ and unit $I := j$) satisfies the five coherence laws of a skew monoidal category, as Theorem 3.1 in:

• Thorsten Altenkirch, James Chapman, Tarmo Uustalu. Monads need not be endofunctors. LMCS 1:3, 2015.

There is a fast and down to earth proof. We use the letters $R$ and $L$ to indicate the right and left adjoints of morphisms.

For the first one, just call $a=j_!x\circ y$ and $b=j_!x\circ j_!y$, we have one morphism $\phi:a\to j^*b$ with left adjoint $L\phi:j_!a\to b$. Then your diagram becomes $$\begin{CD} j^*j_!a @>j^*L\phi>> j^*b\\ @A\eta AA@|\\ a@>\phi>>j^*b \end{CD}$$ which is an easy $1$ categorical fact about adjunction. It's just the right adjoint diagram of $L\phi\circ\text{id}=\text{id}\circ L\phi$, with $\eta=R\text{id}$ and $\phi=RL\phi$.

For the second one, observe that you can prove commutativity before composing with $y$: every arrow has the form $\phi\ast y$ for some $\phi$. Now just use adjunction of $j^*$ and $j_!$: your diagram becomes $$\begin{CD} j_!j\circ x @>Rj_!(\sigma\ast\text{id})>> j^*j_!x\\ @|@A\sigma\ast\text{id} AA\\ j_!j\circ x@>\text{id}\ast\eta>>j_!j\circ j^*j_!x \end{CD}$$

We can now unpack $$Rj_!(\sigma\ast\text{id}):j_!j\circ x\to j^*j_!x$$ as $$j_!j\circ x\xrightarrow{\sigma\ast\text{id}} x\xrightarrow{\eta} j^*j_!x$$ To check that this unpacking is right, just observe that $R\eta=\text{id}$. Hence the diagram above becomes

$$\begin{CD} x @>\eta>> j^*j_!x\\ @A\sigma\ast\text{id} AA@A\sigma\ast\text{id} AA\\ j_!j\circ x@>\sigma\ast\eta>>j_!j\circ j^*j_!x \end{CD}$$ which is obvious.