Elementary doctrines as coalgebras

Lawvere's hyperdoctrines mark the beginning of applications of category theory to logic. In particular, existential elementary doctrines proved essential to give models of non-classical logics. The clear connection between (typed) logical theories and certain -valued functors is exemplified by the embedding of the category of elementary doctrines into that of primary doctrines, which has a right adjoint given by a completion which freely adds quotients for equivalence relations.

We extend that result to show that, in fact, the embedding is 2-functorial and 2-comonadic. As a byproduct we apply the result to produce an algebraic way to extend a first order theory to one which eliminates imaginaries, discuss how it relates to Shelah's original, and show how it works in a wider variety of situations.