The Coq mailing list

[Paolo Herms <paolo.herms AT cea.fr>]

Wow, that was quick.
Thank you, I really didn't see that one.
-- 
Paolo Herms
PhD Student - CEA Software Safety Lab. / Inria ProVal project-team
Paris, France


On Thursday 26 April 2012 17:52:08 gallais @ ensl.org wrote:
> 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