Comonadic adjunction (source code)

= Comonadic adjunction
{wiki=Beck's_monadicity_theorem}

An adjunction is comonadic when the comparison from its left-hand category to coalgebras for the induced comonad is an equivalence. The dual Beck theorem tests this using reflected isomorphisms and suitable equalizers.