Elementary doctrines as coalgebras (Q2220195)

\textit{Hyperdoctrines} were introduced by Lawvere as a categorical way to study logic and in particular \textit{first order theories} [\textit{F. W. Lawvere}, Dialectica 23, 281--296 (1969; Zbl 0341.18002)]. The relation was made precise by Seely, who proved there is an equivalence between categories of first order theories and hyperdoctrines [\textit{R. A. G. Seely}, Z. Math. Logik Grundlagen Math. 29, 505--542 (1983; Zbl 0565.03032)]. Motivated by the desire to present a theory of equivalence relations, Maietti and Rosolini generalized hyperdoctrines to \textit{primary doctrines}, which correspond to first-order theories with binary conjunctions and a true constant, and also introduced the particular case of \textit{elementary doctrines}, which correspond to the aforementioned first order theories with an additional equality predicate [\textit{M. E. Maietti} and \textit{G. Rosolini}, Log. Univers. 7, No. 3, 371--402 (2013; Zbl 1288.03049)]. For example, in [\textit{M. E. Maietti} and \textit{G. Rosolini}, Theory Appl. Categ. 27, 445--463 (2013; Zbl 1288.03048)] Maietti and Rosolini show how to construct an \textit{elementary quotient completion} out of every elementary doctrine. \textit{D. Trotta} [Existential completion and pseudo-distributive laws: an algebraic approach to the completion of doctrines. Università degli Studi di Trento. 89--119 (PhD Thesis) (2019)] showed that that this construction is in fact left adjoint to the inclusion of quotient complete elementary doctrines into elementary doctrines. Trotta also showed the adjunction is \textit{pseudo-monadic}, deducing that elementary doctrines with quotients are pseudo-algebras over elementary doctrines, giving us an elegant application of categorical methods (monads and algebras) to logic (the relation between elementary doctrines and elementary doctrines with quotients). Going in the other direction in [\textit{F. Pasquali}, Appl. Categ. Struct. 23, No. 1, 29--41 (2015; Zbl 1305.03064)] the second author builds on the construction of the elementary quotient completion to construct a \textit{cofree elementary doctrine} out of a primary doctrine by proving it is a right adjoint to the inclusion of elementary doctrines in primary doctrines. The construction of a right adjoint and the pseudo-monadic adjunction by Trotta suggests analyzing the comonadic properties of this adjunction, which is precisely the aim of this paper. In this paper, the authors first prove that the adjunction constructed by the second author is in fact a \(2\)-adjunction between the \(2\)-categories of elementary doctrines and primary doctrines (Proposition \(3.1\)) and then show that this \(2\)-adjunction is \textit{\(2\)-comonadic} (Theorem \(3.2\)), implying that elementary doctrines are simply \(2\)-coalgebras over primary doctrines, opening up the possibility of applying categorical methods (comonads) to the study of elementary doctrines and logic. As a first application the authors prove in Section \(4\) that the cofree elementary doctrine construction can be used to transform every intuitionistic first order theory into one that has \textit{uniform elimination of imaginaries} (Theorem \(4.2\)) as defined in [\textit{B. Poizat}, J. Symb. Log. 48, 1151--1170 (1983; Zbl 0537.03023)] in such a way that every model of the original theory can be turned functorially into a model of the new theory that has uniform elimination of imaginaries (Proposition \(4.3\)). In the final section (Section \(5\)) the results of Section \(4\) are applied to gain a better understanding of \textit{Shelah's construction} [\textit{S. Shelah}, Classification theory and the number of non-isomorphic models. Amsterdam etc.: North-Holland (1990; Zbl 0713.03013)], which in [\textit{V. Harnik}, in: Models, logics, and higher-dimensional categories: A tribute to the work of Mihály Makkai. Proceedings of a conference, CRM, Montréal, Canada, June 18--20, 2009. Providence, RI: American Mathematical Society (AMS). 79--106 (2011; Zbl 1243.03080)] was proven by Harnik to correspond to \textit{pretopos completion}. In fact in Proposition \(5.1\) (which is proven in Appendix \(A\)) the authors give an alternative characterization of the pretopos completion and then apply that to the results of Section \(4\) to get Shelah's construction for general intuitionistic first order theories.