The Coq mailing list

[jd AT sophia.inria.fr (Joelle Despeyroux)]

|> Je suis (presque) sur que non. Je ne me suis jamais mis a` faire la
|> preuve en detail, mais je crois que on peut tres facilement adapter
|> celle que Martin Hofmann a fait dans la section 6.2 de sa these:
|> 
|> @PHDTHESIS{MH95,
|>         AUTHOR          = {M. Hofmann},
|>         SCHOOL          = {University of Edinburgh},
|>         TITLE           = {Extensional Concepts in Intentional Type 
Theory},
|>         YEAR            = {1995},
|>         key             = {ECS-LFCS-95-327},
|>         month           = {July}
|> }
|> 
|> L'axiome ne gene pas a` l'extraction non plus, car tout se passe dans
|> l'univers des propositions.

hence the question, which often comes: 
does someone plan to implement M. Hofmann's work for Coq? 

This would make the proofs much easier, both in semantics and in 
mathematics.
Martin Hofmann told me he was interested in doing the job at a time, 
but finally did not find time for it... Maybe he would be interested 
in participating to the task? This would be great!

  Joelle Despeyroux