The notion of a comonadic functor is the dual of that of a monadic functor. See there for more background.
Given a pair $L\dashv R$ of adjoint functors, $L\colon A \to B\colon R$, with counit $\epsilon$ and unit $\eta$, one forms a comonad $\mathbf{\Omega} = (\Omega, \delta, \epsilon)$ by $\Omega \coloneqq L \circ R$, $\delta \coloneqq L \eta R$. $\mathbf{\Omega}$-comodules (aka $\mathbf{\Omega}$-coalgebras) form a category $B_{\mathbf{\Omega}}$ and there is a natural comparison functor $K = K_{\mathbf{\Omega}}\colon A \to B_{\mathbf{\Omega}}$ given by $A \mapsto (L A, L A \stackrel{L(\eta_A)}\to L R L A)$.
A functor $L\colon A\to B$ is comonadic if it has a right adjoint $R$ and the corresponding comparison functor $K$ is an equivalence of categories. The adjunction $L \dashv R$ is said to be a comonadic adjunction.
Beck’s monadicity theorem has its dual, comonadic analogue. To discuss it, observe that for every $\Omega$-comodule $(N, \rho)$,
manifestly exhibits a split equalizer sequence.
…
If $T: Set \to Set$ is a monad on $Set$, with corresponding monadic functor $U: Set^T \to Set$, then the left adjoint $F: Set \to Set^T$ is comonadic provided that $F(!): F(0) \to F(1)$ is a regular monomorphism and not an isomorphism. In particular, if $T$ is given by an algebraic theory with at least one constant symbol and at least one function symbol of arity greater than zero, then the left adjoint is comonadic (because then $F(!): F(0) \to F(1)$ is a split monomorphism but not an isomorphism).
More generally, let $A$ be a locally small category with small copowers, and suppose $a$ is an object such that $0 \to a$ is a regular monomorphism but not an isomorphism, then the copowering with $a$,
(left adjoint to $A(a, -): A \to Set$) is comonadic. See proposition 6.13 and related results in this paper by Mesablishvili.
In the context of the treatment of modal operators given at Possible worlds via first-order logic and type theory, we find that base change along the terminal morphism from the type of worlds, $W$, and its right adjoint, dependent product, form a comonadic adjunction. $W^{\ast} \dashv \prod_W$.
Let $\mathbf{H}$ be a topos. For a type/object, $P$, in $\mathbf{H} \simeq \mathbf{H}_{/\ast}$ we have that
(projection on the second component). And for $[Q \to W]$ in $\mathbf{H}_{/W}$, we have
Hence the composite, a kind of necessity operator
(an analog of the jet comonad), sends $Q \to W$ to $\Gamma_W(Q) \times W \to W$.
If $W$ is an inhabited object so that $W \to \ast$ is an epimorphism, then $W^\ast$ is a conservative functor. Since it moreover preserves all limits (having a further left adjoint, the dependent sum operation) the monadicity theorem applies and says that the coalgebras for this comonad are the types in $\mathbf{H}$, or rather the types in $\mathbf{H}_{/W}$ which are in the image of $W^{\ast}$, hence of the form $P \times W$, and equipped with the map
over $W$ ($P^W$ denotes the internal hom), where the first component of the map sends $p: P$ to the constant map at $p$.
To see this as an equalizer, consider the two maps from $\Box_W (P \times W \to W)$ to $\Box_W \Box_W (P \times W \to W)$. Over $W$, these are formed from the two ways of mapping $P^W$ to $P^{(W \times W)}$, by sending $f$ in $P^W$ to $g \colon (w, w') \mapsto f(w)$ and to $h \colon (w, w') \mapsto f(w')$.
The equalizer of these two maps is formed from the $f$ for which $g = h$ for all $w, w'$ in $W$, that is, when $f$ is constant. So the equalizer is equivalent to $W^{\ast} P = P \times W \to W$.
monadic functor, comonadic functor