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 Pos-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. (C) 2020 Elsevier B.V. All rights reserved.

[发布日期] 2020-12-01

[关键词] Elementary doctrine;2-Comonad;Quotient completion;Elimination of imaginaries