%0 Conference Proceedings %1 citeulike:1019373 %A Altenkirch, T. %D 1999 %J Logic in Computer Science, 1999. Proceedings. 14th Symposium on %K theory type %P 412--420 %T Extensional equality in intensional type theory %U http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=782636 %X 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 Πand Σ-types. The Type Theory corresponding to this model is decidable, has no irreducible constants and permits large eliminations, which are essential for universes

@proceedings{citeulike:1019373, 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 \η-rules for \Πand \Σ-types. The Type Theory corresponding to this model is decidable, has no irreducible constants and permits large eliminations, which are essential for universes}, added-at = {2007-08-18T13:22:24.000+0200}, author = {Altenkirch, T.}, biburl = {https://www.bibsonomy.org/bibtex/2a037ceedca96a26a477efcc46b6ef413/a_olympia}, citeulike-article-id = {1019373}, description = {citeulike}, interhash = {f248a116e7cd99e9e71b9b2ba298eefe}, intrahash = {a037ceedca96a26a477efcc46b6ef413}, journal = {Logic in Computer Science, 1999. Proceedings. 14th Symposium on}, keywords = {theory type}, pages = {412--420}, priority = {2}, timestamp = {2007-08-18T13:22:32.000+0200}, title = {Extensional equality in intensional type theory}, url = {http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=782636}, year = 1999 }