coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: extensionnalite

From: Jean-Christophe Filliatre <filliatr AT lri.fr>
To: Henri Fraisse <henri.fraisse AT trusted-logic.fr>
Cc: coq AT pauillac.inria.fr
Subject: Re: extensionnalite
Date: Mon, 27 Sep 1999 14:06:28 +0200 (MEST)

> Ca doit sans doute etre tres simple, mais je ne vois pas comment
> montrer l'axiome d'extensionnalite pour les fonctions, a savoir:
>
> Lemma ext:(A,B:Set)(f,g:A->B)((a:A)(f a)=(g a))->f=g.

This is not provable, since this not true. Indeed, equality means here
convertibility  and you  may  have two  functions extensionally  equal
without being convertible (as terms).

--
Jean-Christophe FILLIATRE

mailto:Jean-Christophe.Filliatre AT lri.fr
  http://www.lri.fr/~filliatr

extensionnalite, Henri Fraisse
- Re: extensionnalite, Jean-Christophe Filliatre
  - Re: extensionnalite, Judicael Courant
- Re: extensionnalite, Benjamin Werner
- Re: extensionnalite, Healfdene Goguen