Elementary doctrines as coalgebras

Research output: Contribution to journalArticlepeer-review

Authors

Colleges, School and Institutes

Abstract

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.

Details

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

Keywords

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

ASJC Scopus subject areas