Elementary quotient completion
Maria Emilia Maietti, Giuseppe Rosolini · Theory and applications of categories · 2013
We extend the notion of exact completion on a category with weak finite limits to Lawvere's elementary doctrines.We show how any such doctrine admits an elementary quotient completion, which is the universal solution to adding certain quotients.We note that the elementary quotient completion can be obtained as the composite of two other universal constructions: one adds effective quotients, the other forces extensionality of morphisms.We also prove that each construction preserves comprehension.