I'm going through the Elephant but I'm having a hard time verifying a given structure satisfies the comonad conditions.
Let $\mathbb{C}$ be some internal category in $\mathcal{S}$ and $\mathbb{D}$ an $\mathcal{S}$-indexed category which is $\mathcal{S}$-complete. The author defines the following comonad structure on $M = \Pi_{d_0} d_1^\ast$:
(for notation, $(\theta, \phi_{g, f}$), $(\Theta, \psi_{g, f})$ are the unit and composition isos for $x^\ast$ and $\Pi_x$, respectively)
Counit: $$\eta^\prime = (\Theta^{-1} \psi_{d_0, i} \ast \theta^{-1} \phi_{d_1, i}) \circ \Pi_{d_0} \eta^i_{d_1^\ast}$$
Comultiplication $$\mu^\prime = \Pi_{d_0} \alpha_{d_1^\ast} \circ (\psi^{-1}_{d_0, p_0} \psi_{d_0, c} \ast \phi^{-1}_{d_1, p_1} \phi_{d_1, c}) \circ \Pi_{d_0} \eta^c_{d_1^\ast}$$
where $\alpha$ is induced by the Beck-Chevalley condition on the pullback giving $C_2$:
I'm struggling to prove something as simple as $\Pi_{d_0} d_1^\ast \eta^\prime \circ \mu^\prime = 1$.
I rewrote the equation several times, expanded the expressions, but to no avail. Every equation sequence I write gets me stuck at certain point. The author comments it is straightforward from the commutativity of diagrams in the definition of an internal category, but I'm not sure if that means something specific, like using $c (1 \times i d_0) = 1$ to prove this specific identity.
For instance, I thought (this is on the level of intuition) that the expression could be a backwards $c (1 \times i d_0)$ if we wrote something like $\square(f) = (\psi_{g, f} \ast \phi_{g, f}) \circ \Pi_{d_0} \eta^f_{d_1^\ast}$ and resolved some sort of composition rule which would give us $\square(c(1 \times id_0)) = \square(1) = 1$, but this is just an idea, something to look at the expression as given by a composition of expressions based on arrows with some sort of identity wrt composition and products, if that's what the author meant about using the commutativity conditions.
Anyway, I'd appreciate if someone could give me a hint, be it some brute-force solution for instance or some hint for an approach based on the "big picture" of the expression (especially since I'll still need to check associativity). Any help is appreciated!
EDIT: Here's an example of my attempts:
\begin{align*}
\Pi_{d_0} d_1^\ast \eta^\prime \circ \mu^\prime
\\ = \Pi_{d_0} d_1^\ast (\Theta^{-1} \psi_{d_0, i} \ast \theta^{-1} \phi_{d_1, i}) \circ \Pi_{d_0} d_1^\ast \Pi_{d_0} \eta^i_{d_1^\ast} \circ \Pi_{d_0} \alpha_{d_1^\ast} \circ (\psi^{-1}_{d_0, p_0} \psi_{d_0, c} \ast \phi^{-1}_{d_1, p_1} \phi_{d_1, c}) \circ \Pi_{d_0} \eta^c_{d_1^\ast}
\\ = \Pi_{d_0} d_1^\ast (\Theta^{-1} \psi_{d_0, i} \ast \theta^{-1} \phi_{d_1, i}) \circ \color{red}{\Pi_{d_0} \alpha_{\Pi_i i^\ast d_1^\ast} \circ \Pi_{d_0} \Pi_{p_0} p_1^\ast \eta^i_{d_1^\ast}} \circ (\psi^{-1}_{d_0, p_0} \psi_{d_0, c} \ast \phi^{-1}_{d_1, p_1} \phi_{d_1, c}) \circ \Pi_{d_0} \eta^c_{d_1^\ast} && \text{(1)}
\\ = \Pi_{d_0} d_1^\ast (\Theta^{-1} \psi_{d_0, i} \ast \theta^{-1} \phi_{d_1, i}) \circ \Pi_{d_0} \alpha_{\Pi_i i^\ast d_1^\ast} \circ \color{red}{(\psi^{-1}_{d_0, p_0} \psi_{d_0, c})_{p_1^\ast \Pi_i i^\ast d_1^\ast} \circ \Pi_{d_0} \Pi_{c} p_1^\ast \eta^i_{d_1^\ast}} \circ \Pi_{d_0} \Pi_{c} \phi^{-1}_{d_1, p_1} \phi_{d_1, c} \circ \Pi_{d_0} \eta^c_{d_1^\ast} && \text{(2)}
\\ = \Pi_{d_0} d_1^\ast \Theta^{-1} \psi_{d_0, i} \circ \color{red}{\Pi_{d_0} \alpha_{\Pi_i} \circ \Pi_{d_0} \Pi_{p_0} p_1^\ast \Pi_i \theta^{-1} \phi_{d_1, i}} \circ (\psi^{-1}_{d_0, p_0} \psi_{d_0, c})_{p_1^\ast \Pi_i i^\ast d_1^\ast} \circ \Pi_{d_0} \Pi_{c} p_1^\ast \eta^i_{d_1^\ast} \circ \Pi_{d_0} \Pi_{c} \phi^{-1}_{d_1, p_1} \phi_{d_1, c} \circ \Pi_{d_0} \eta^c_{d_1^\ast} && \text{(3)}
\\ = \Pi_{d_0} d_1^\ast \Theta^{-1} \psi_{d_0, i} \circ \Pi_{d_0} \alpha_{\Pi_i} \circ \color{red}{(\psi^{-1}_{d_0, p_0} \psi_{d_0, c})_{p_1^\ast \Pi_i} \circ \Pi_{d_0} \Pi_{c} p_1^\ast \Pi_i \theta^{-1} \phi_{d_1, i}} \circ \Pi_{d_0} \Pi_{c} p_1^\ast \eta^i_{d_1^\ast} \circ \Pi_{d_0} \Pi_{c} \phi^{-1}_{d_1, p_1} \phi_{d_1, c} \circ \Pi_{d_0} \eta^c_{d_1^\ast} && \text{(4)}
\end{align*}
(1): Naturality of $\alpha$
(2): Naturality of $\psi^{-1}_{d_0, p_0} \psi_{d_0, c}$
(3): Naturality of $\alpha$
(4): Naturality of $\psi^{-1}_{d_0, p_0} \psi_{d_0, c}$
I then proceeded to expand the expressions but got nowhere. I'll omit the rest to keep it tidy, but I arrived at something like
\begin{align*} \left( \Pi_{d_0} \Pi_{c} p_1^\ast \ast (\Pi_i \phi_{d_0, i} \circ \eta^i_{d_0^\ast} ) \circ \Pi_{d_0} \Pi_c {\phi^{-1}_{d_0, p_1} \phi_{d_1, p_0}} \circ \Pi_{d_0} \mathrm{Mate}(\phi_{{d_0}, {p_0}}^{-1} \circ \phi_{{d_0}, {c}})_{d_1^\ast} \circ \eta^{d_0}_{\Pi_{d_0} d_1^\ast} \right)^{-1} \\ \circ \Pi_{d_0} \Pi_{c} p_1^\ast \Pi_i \phi_{d_1, i} \circ \Pi_{d_0} \Pi_{c} p_1^\ast \eta^i_{d_1^\ast} \circ \Pi_{d_0} \Pi_{c} \phi^{-1}_{d_1, p_1} \phi_{d_1, c} \circ \Pi_{d_0} \eta^c_{d_1^\ast} \end{align*}
Given a pair of objects $X$ and $Y$ of category $C$, its category of spans has for its objects pairs $s\colon S\to X,t\colon S\to Y$ of morphisms with common domain, and for its morphisms from a span $s'\colon T\to X,t'\colon T\to Y$ to a span $s\colon S\to X,t\colon S\to Y$ the morphisms $f\colon T\to S$ for which $t'=t\circ f$ and $s'=s\circ f$.
A bifibration $D\to C$ with functors sending morphisms $f\colon X\to Y$ to $f_*\colon D^X\to D^Y$ and $f^*\colon D^X\leftarrow D^Y$, determines for each span $X\overset s\leftarrow S\overset t\to Y$ a functor $t_*s^*\colon C/X\to C/Y$.
If $f_*$ are left adjoint to $f^*$ with counit $\epsilon_f\colon f_*f^*\Rightarrow\mathrm{id}$, then a morphism $f\colon T\to S$ of spans from $X\overset s\leftarrow S\overset f\leftarrow T\overset f\to S\overset t\to Y$ to $X\overset s\leftarrow S\overset t\to Y$, determines a natural transformation $e_f\colon (tf)_*(sf)^*\cong t_*f_*f^*s^*\overset{t_*\epsilon_fs^*}\longrightarrow t_*s^*$.
If $f_*$ is right adjoint to $f_*$ with unit $\eta_f\colon\mathrm{id}\Rightarrow f_*f^*$, then a morphism $f\colon T\to S$ of spans from $X\overset s\leftarrow S\overset f\leftarrow T\overset f\to S\overset t\to Y$ to $X\overset s\leftarrow S\overset t\to Y$, determines a natural transformation $u_f\colon t_*s^*\overset{t_*u_fs^*}\longrightarrow t_*f_*t^*f^*\cong (tf)_*(sf)^*$.
Moreover, the above determinations are in fact functorial. Thus, a bifibration $D\to C$ determines either a covariant or contravariant functor from the category of spans over $X$ and $Y$ to the category of functors $D^X\to D^Y$, the variance depending on whether $f_*$ is left or right adjoint to $f^*$.
Next, given two spans $X\overset{s_1}\leftarrow S_1\overset{t_1}\to Y$ and $Y\overset{s_2}\leftarrow S_2\overset{t_2}\to Z$, their composite, if it exists, is $X\overset{s_1}\leftarrow S_1\overset{s_3}\leftarrow S_3\overset{t_3}\to S_2\overset{t_2}\to T_2$ where $t_1\circ s_3=s_2\circ t_3$ is a pullback square.
The Beck-Chevalley condition implies that morphisms of spans out of the composite span correspond to natural transformations out of (or into for the contravariant case) the composite functor ${t_2}_*s_2^*{t_1}_*s_1^*\colon D^X\to D^Z$.
Now a category is a span $C_0\overset{d_0}\leftarrow C_1\overset{d_1}\to C_1$ equipped with a morphism of spans from $C_0\overset{\mathrm{id}}\leftarrow C_0\overset{\mathrm{id}}\to C_0$ and from its composite with itself, satisfying equations expressing identity and associativity of composition. The span then determines a functor $D^{C_0}\to D^{C_0}$, and the morphisms of spans determine natural transformations from (or into in the contravariant case) the identity functor $D^{C_0}\to D^{C_0}$ and the self-composite $D^{C_0}\to D^{C_0}\to D^{C_0}$. Moreover, these must also satisfy the equation of identity and associativity. But that's exactly the definition of a monad (or comonad in the contravariant case).