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 Symposium on Logic in Computer Science (LICS 1999)},
    year =	 {1999},
    month =	 {July}, 
    pages =      {412--420},
    location =   {Trento, Italy}, 
    publisher =	 {IEEE Computer Society Press}
  }