## Paper: Extensional Equality in Intensional Type Theory (at LICS 1999)

Authors:**Thorsten Altenkirch**

### 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 eta-rules for Pi- and Sigma-types. The Type Theory corresponding to this model is decidable, has no irreducible constants and permits large eliminations, which are essential for universes.

### BibTeX

@InProceedings{Altenkirch-ExtensionalEquality, author = {Thorsten Altenkirch}, title = {Extensional Equality in Intensional Type Theory}, booktitle = {Proceedings of the Fourteenth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1999}, year = 1999, editor = {Giuseppe Longo}, month = {July}, pages = {412--420}, location = {Trento, Italy}, publisher = {IEEE Computer Society Press} }