Let $\mathbb{D}$ be an $\mathcal{S}$-indexed category which has $\mathcal{S}$-indexed products. I'm trying to follow an argument relating comonads to internal diagrams, and it seems that I need the following identity:
$$(\Theta^{-1} \psi_{d_0, i} \ast \theta^{-1} \phi_{d_0, i}) \circ \Pi_{d_0} \eta^i_{d_0^\ast} \circ \eta^{d_0} = 1$$
where $d_0, d_1: C_1 \to C_0$ are domain and codomain and $i: C_0 \to C_1$ the identity map of an internal category in $\mathcal{S}$, and $\Theta, \psi$ and $\theta, \phi$ the identity and composition coherence isos for $\Pi_x, x^\ast$, respectively, while $\eta^x$ denotes the unit for $x^\ast \dashv \Pi_x$.
My closest guess (assuming the identity holds) is some suitable pullback square so I can apply the Beck-Chevalley condition, but I'm clueless on this. Does this identity hold, or even in more generality, does
$$(\Theta^{-1} \ast \theta^{-1}) \circ \eta^1 = 1$$
$$(\psi_{g, f} \ast \phi_{g, f}) \circ \Pi_{g} \eta^f_{g^\ast} \circ \eta^g = \eta^{gf}$$
holds? How can I prove these identities?
Any help is appreciated!
Okay nevermind, I guess I just needed to compute the expressions that give the coherence isos for $\Pi_x$:
$$ \Theta^{-1} = \epsilon^1 \circ \theta_{\Pi_1}$$
hence
$$(\Theta^{-1} \ast \theta^{-1}) \circ \eta^1 = \theta^{-1} \circ \epsilon^1_{1^\ast} \circ \theta_{\Pi_1 1^\ast} \circ \eta^1 = 1$$
Also,
$$\psi_{x, y} = \Pi_{yx} \epsilon^x \circ \Pi_{yx} x^\ast \epsilon^y_{\Pi_x} \circ \Pi_{yx} {\phi^{-1}_{y, x}}_{\Pi_y \Pi_x} \circ \eta^{yx}_{\Pi_y \Pi_x}$$
so
\begin{align*} (\psi_{y, x} \ast \phi_{y, x}) \circ \Pi_y \eta^x_{y^\ast} \circ \eta^y \\ = \Pi_{yx} \phi_{y, x} \circ [(\Pi_{yx} \epsilon^x \circ \Pi_{yx} x^\ast \epsilon^y_{\Pi_x} \circ \Pi_{yx} {\phi^{-1}_{y, x}}_{\Pi_y \Pi_x} \circ \eta^{yx}_{\Pi_y \Pi_x}) \ast (x^\ast y^\ast)] \circ \Pi_y \eta^x_{y^\ast} \circ \eta^y \\ = \Pi_{yx} \phi_{y, x} \circ [(\Pi_{yx} \epsilon^x \circ \Pi_{yx} x^\ast \epsilon^y_{\Pi_x} \circ \Pi_{yx} {\phi^{-1}_{y, x}}_{\Pi_y \Pi_x}) \ast (x^\ast y^\ast)] \circ \Pi_{yx} {(yx)}^\ast \Pi_y \eta^x_{y^\ast} \circ \eta^{yx}_{\Pi_y y^\ast} \circ \eta^y && \text{(1)} \\ = \Pi_{yx} \phi_{y, x} \circ [(\Pi_{yx} \epsilon^x \circ \Pi_{yx} x^\ast \epsilon^y_{\Pi_x}) \ast (x^\ast y^\ast)] \circ \Pi_{yx} x^\ast y^\ast \Pi_y \eta^x_{y^\ast} \circ \Pi_{yx} {\phi^{-1}_{y, x}}_{\Pi_y y^\ast} \circ \eta^{yx}_{\Pi_y y^\ast} \circ \eta^y && \text{(2)} \\ = \Pi_{yx} \phi_{y, x} \circ [(\Pi_{yx} \epsilon^x) \ast (x^\ast y^\ast)] \circ \Pi_{yx} x^\ast \eta^x_{y^\ast} \circ \Pi_{yx} x^\ast \epsilon^y_{y^\ast} \circ \Pi_{yx} {\phi^{-1}_{y, x}}_{\Pi_y y^\ast} \circ \eta^{yx}_{\Pi_y y^\ast} \circ \eta^y && \text{(3)} \\ = \Pi_{yx} \phi_{y, x} \circ \Pi_{yx} x^\ast \epsilon^y_{y^\ast} \circ \Pi_{yx} {\phi^{-1}_{y, x}}_{\Pi_y y^\ast} \circ \eta^{yx}_{\Pi_y y^\ast} \circ \eta^y && \text{(4)} \\ = \Pi_{yx} \phi_{y, x} \circ \Pi_{yx} x^\ast \epsilon^y_{y^\ast} \circ \Pi_{yx} {\phi^{-1}_{y, x}}_{\Pi_y y^\ast} \circ \Pi_{yx} {(yx)}^\ast \eta^y \circ \eta^{yx} && \text{(5)} \\ = \Pi_{yx} \phi_{y, x} \circ \Pi_{yx} x^\ast \epsilon^y_{y^\ast} \circ \Pi_{yx} x^\ast y^\ast \eta^y \circ \Pi_{yx} {\phi^{-1}_{y, x}}\circ \eta^{yx} && \text{(6)} \\ = \eta^{yx} && \text{(7)} \end{align*}
$(1)$: Naturality of $\eta^{yx}$
$(2)$: Naturality of $\phi_{y, x}^{-1}$
$(3)$: Naturality of $\epsilon^y$
$(4)$: Triangle identity for $x$
$(5)$: Naturality of $\eta^{yx}$
$(6)$: Naturality of $\phi_{y, x}^{-1}$
$(7)$: Triangle identity for $y$
That one's on me being lazy.