Quotients over Minimal Type Theory

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 `a 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.

• Type: Conference
• Year: 2007
• Where: CIE
• Authors: Maria Emilia Maietti
• Keywords: CIE 2007, Effective Quotient Sets, Extensional Type Theory, Type Theory MTT