Extensional Equality in Intensional Type Theory

We present a new approach to introducing an extensional propositional equality in Intensional Type Theory. Our construction is based on the observation that there is a sound, intensional setoid model in Intensional Type theory with a proof-irrelevant universe of propositions and -rules for

• Type: Conference
• Year: 1999
• Where: LICS
• Authors: Thorsten Altenkirch
• Keywords: Automated Reasoning, Extensional Propositional Equality, Intensional Type Theory, LICS 1999, Type Theory