Elementary doctrines as coalgebras

Research output: Contribution to journalArticlepeer-review


Colleges, School and Institutes


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.


Original languageEnglish
Article number106445
JournalJournal of Pure and Applied Algebra
Issue number12
Early online date18 May 2020
Publication statusPublished - Dec 2020


  • Elementary doctrine, 2-Comonad, Quotient completion, Elimination of imaginaries

ASJC Scopus subject areas