An algebraic approach to the completions of elementary doctrines

We provide a thorough algebraic analysis of three known completions having a central role in the exact completions of Lawvere’s doctrines, the one adding comprehensive diagonals (i.e. forcing equality on terms to coincide with the equality predicate), the one adding full comprehensions and the one adding quotients. We show that all these 2-adjunctions are 2-monadic and that the 2-monads arising from these adjunctions are all property-like. This entails that comprehensive diagonals, full comprehensions and quotients are algebraic properties of an elementary doctrine. Finally, we discuss and present the distributive laws between these 2-monads.

Davide Trotta
Davide Trotta
Postdoc

I am a mathematician, and my research is mainly focused on categorical logic and its applications in theoretical computer science.