Extensional equality in intensional type theory
- 20 January 2003
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- p. 412-420
- https://doi.org/10.1109/lics.1999.782636
Abstract
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 /spl eta/-rules for /spl Pi/and /spl Sigma/-types. The Type Theory corresponding to this model is decidable, has no irreducible constants and permits large eliminations, which are essential for universes.Keywords
This publication has 3 references indexed in Scilit:
- A general formulation of simultaneous inductive-recursive definitions in type theoryThe Journal of Symbolic Logic, 2000
- Internal type theoryPublished by Springer Nature ,1996
- A simple model for quotient typesPublished by Springer Nature ,1995