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.
Keywords: quotient completion, split fibration, universal construction
2010 MSC: 03G30 03B15 18C50 03B20 03F55
Theory and Applications of Categories, Vol. 27, 2013, No. 17, pp 445-463.
Published 2013-09-08
http://www.tac.mta.ca/tac/volumes/27/17/27-17.dvi
http://www.tac.mta.ca/tac/volumes/27/17/27-17.ps
http://www.tac.mta.ca/tac/volumes/27/17/27-17.pdf
ftp://ftp.tac.mta.ca/pub/tac/html/volumes/27/17/27-17.dvi
ftp://ftp.tac.mta.ca/pub/tac/html/volumes/27/17/27-17.ps