The Coq mailing list

["gallais @ ensl.org" <guillaume.allais AT ens-lyon.org>]

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
>
>