Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Type extensionality?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Type extensionality?


chronological Thread 
  • From: "gallais @ ensl.org" <guillaume.allais AT ens-lyon.org>
  • To: Paolo Herms <paolo.herms AT cea.fr>
  • Cc: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Type extensionality?
  • Date: Thu, 26 Apr 2012 16:51:37 +0100

Hi Paolo,

Your [type_extensionality] is a consequence of dependent functional
extensionality so it should be safe.

The axiom is taken from:
http://coq.inria.fr/stdlib/Coq.Logic.FunctionalExtensionality.html

====================
Axiom functional_extensionality_dep : forall {A} {B : A -> Type},
  forall (f g : forall x : A, B x),
  (forall x, f x = g x) -> f = g.

Lemma type_extensionality :  forall A (T1: A -> Type) (T2: A -> Type),
   (forall a, T1 a = T2 a) -> (forall a, T1 a) = (forall a, T2 a).
Proof.
intros A T1 T2 Heq.
 rewrite (@functional_extensionality_dep A (fun _ => Type) T1 T2).
 reflexivity.
 assumption.
Qed.
====================

Cheers,

--
guillaume


On 26 April 2012 16:35, Paolo Herms 
<paolo.herms AT cea.fr>
 wrote:
> Hello,
> do you think this can be proved in Coq under some conditions or can it be
> safely assumed as an axiom?
>
> Conjecture type_extensionality :  forall A (T1: A -> Type) (T2: A -> Type),
>    (forall a, T1 a = T2 a) -> (forall a, T1 a) = (forall a, T2 a).
>
> Thanks for any idea,
> --
> Paolo Herms
> PhD Student - CEA Software Safety Lab. / Inria ProVal project-team
> Paris, France
>
>




Archive powered by MhonArc 2.6.16.

Top of Page