The Coq mailing list

[Healfdene Goguen <hhg AT att.com>]

Martin Hofmann has demonstrated in his thesis [2] the validity of
extensionality, and more generally quotient types, in intensional type
theory by interpreting the axioms and equalities for these types into
intensional type theory with an (intensional) equality slightly
stronger than that of Coq.  Essentially, every closed type is
interpreted by a type and an equivalence relation.

The original approach had some weaknesses in the treatment of
universes.  Thorsten Altenkirch [1] more recently refined the
technique so that it works for large eliminations as well.

Yours,
Healf Goguen

[1] Thorsten Altenkirch.  Extensional Equality in Intensional Type
Theory.  LICS 1999.

[2] Martin Hofmann.  Extensional Concepts in Intensional Type Theory.
Ph.D. thesis, University of Edinburgh, July 1995.