Quotient completion for the foundation of constructive mathematics
Logic
2013-12-04 v2 Category Theory
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.
Keywords
Cite
@article{arxiv.1202.1012,
title = {Quotient completion for the foundation of constructive mathematics},
author = {Maria Emilia Maietti and Giuseppe Rosolini},
journal= {arXiv preprint arXiv:1202.1012},
year = {2013}
}
Comments
32 pages