Elementary quotient completion

TL;DR

This paper introduces a new construction called elementary quotient completion for elementary doctrines, which systematically adds effective quotients and extensional equality, enhancing the categorical structure.

Contribution

It extends exact completion to elementary doctrines and shows how to freely add effective quotients and extensionality through a composite construction.

Findings

Elementary quotient completion admits effective quotients.

The construction preserves comprehensions.

It can be decomposed into two free constructions: adding quotients and extensionality.

Abstract

We extend the notion of exact completion on a weakly lex category to elementary doctrines. We show how any such doctrine admits an elementary quotient completion, which freely adds effective quotients and extensional equality. We note that the elementary quotient completion can be obtained as the composite of two free constructions: one adds effective quotients, and the other forces extensionality of maps. We also prove that each construction preserves comprehensions.