$\require{AMScd}$Let $\cal K$ be a 2-category, and $j : A\to B$ one of its 1-cells. Assume that the induced map $$ j^* : {\cal K}(B,B)\to {\cal K}(A,B) $$ precomposing with $j$ has a left adjoint $j_!$, the left extension along $j$.
Given 1-cells $x,y\in {\cal K}(A,B)$, it is possible to obtain canonical maps
- $\gamma_{xyz} : j_! (j_!x\circ y) \circ z \to j_!x\circ j_!y\circ z$, a map that in turn is determined by a map $\bar\gamma : j_!(j_!x\circ y) \to j_!x\circ j_! y$ via the universal property of $j_!$, so that $\gamma = \bar\gamma * z$; in ${\cal K}=\bf Cat$, a sufficient condition for this to be invertible is that left extensions along $j$ are absolute.
- $\sigma : j_!(j)\to 1_B$ the counit of the density comonad of $j$; in ${\cal K}=\bf Cat$, this is invertible if and only if $j$ is dense.
- $\eta : x \to j_!(x)\circ j$, the $x$-component of the unit of $j_!\dashv j^*$; in ${\cal K}=\bf Cat$, this is invertible if and only if $j$ is fully faithful.
I want to prove that the following two diagrams of 2-cells are commutative: $$ \begin{CD} j_!(j_!x\circ y)\circ j @>\gamma_{xyj}>> j_!x\circ j_!y\circ j\\ @A\eta_{j_!x\circ y}AA @| \\ j_!(x)\circ y @>>j_!x * \eta_y> j_!x\circ j_!y\circ j \end{CD} \begin{CD} j_!(j_!j\circ x)\circ y @>j_!\sigma * y>> j_!x\circ y \\ @| @AA\sigma * j_!x\circ y A \\ j_!(j_!j\circ x)\circ y @>>\gamma_{jxy}> j_!j\circ j_!x \circ y \end{CD} $$ But, as I expected when I began, this is going to be quite painful. Any advice to make the proof simpler and clearer?
A conceptual proof in ${\cal K}=\bf Cat$, that can be adapted to a generic $\cal K$, is welcome!
Edit (Jul 23, 2018). What I am trying to prove is that the claim that appears as Theorem 3.1 in "Monads need not be endofunctors" holds in a generic 2-category.
