The Coq mailing list

[Haixing Hu <Haixing.Hu AT imag.fr>]

Yes, I think you can add this axiom to the system. This is just what Turner
has done. You can refer to the following article for details. 

David A. Turner. "A new formulation of constructive type theory". In Peter
Dybjer et al., editors, Proceedings of the Workshop on Programming
Logic. Programming Methodology Group, University of Goteborg and
Chalmers University of Technology, 1989. Technical Report, number 54.


On Thu, Feb 10, 2005 at 10:49:48AM -0500, Steve Zdancewic wrote:
> Hi everyone,
> 
> Is there a technical reason why there is no extensional equality 
> principle for function types?  The base library has surjective pairing 
> for products, but nothing like this axiom:
> 
> Axiom extensionality : forall (A:Set) (B:Set) (f:A->B)(g:A ->B),
>   (forall x:A, f x = g x) -> f = g.
> 
> Connor McBride's recent post (in the thread "Cannot Rewrite Under 
> Lambda") indicates that it is not possible to prove this as a lemma, but 
> does adding this axiom lead to inconsistencies?
> 
> Thanks,
> 
> Steve Zdancewic
> Dept. Computer and Information Science
> University of Pennsylvania
> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>          http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

-- 
Haixing Hu.     Equipe cadp. VERIMAG. Grenoble. France.