Elementary doctrines as coalgebras

Jacopo Emmenegger, Fabio Pasquali, Giuseppe Rosolini

Research output: Contribution to journalArticlepeer-review

1 Citation (Scopus)
215 Downloads (Pure)


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

  • Algebra and Number Theory


Dive into the research topics of 'Elementary doctrines as coalgebras'. Together they form a unique fingerprint.

Cite this