Abstract
We consider an extensional version, called qmTT, of the intensional Minimal Type Theory mTT, introduced in a previous paper with G. Sambin, enriched with proof-irrelevance of propositions and effective quotient sets. Then, by using the construction of total setoid à la Bishop we build a model of qmTT over mTT. The design of an extensional type theory with quotients and its interpretation in mTT is a key technical step in order to build a two level system to serve as a minimal foundation for constructive mathematics as advocated in the mentioned paper about mTT. © Springer-Verlag Berlin Heidelberg 2007.
Author supplied keywords
Cite
CITATION STYLE
Maietti, M. E. (2007). Quotients over minimal type theory. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4497 LNCS, pp. 517–531). https://doi.org/10.1007/978-3-540-73001-9_54
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
