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