Quotient completion for the foundation of constructive mathematics

TL;DR

This paper introduces a categorical framework using Lawvere hyperdoctrines and quotient completion to formalize constructive mathematics within intensional type theory, unifying various existing constructions.

Contribution

It develops an abstract categorical approach to quotient completion, encompassing exact completion and type-theoretic examples, advancing the foundations of constructive mathematics.

Findings

Unified categorical framework for quotient completion

Includes exact completion and type-theoretic examples

Provides new insights into formalizing constructive mathematics

Abstract

We apply some tools developed in categorical logic to give an abstract description of constructions used to formalize constructive mathematics in foundations based on intensional type theory. The key concept we employ is that of a Lawvere hyperdoctrine for which we describe a notion of quotient completion. That notion includes the exact completion on a category with weak finite limits as an instance as well as examples from type theory that fall apart from this.