coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
>
>
- [Coq-Club] Type extensionality?, Paolo Herms
- Re: [Coq-Club] Type extensionality?, gallais @ ensl.org
- Message not available
- Re: [Coq-Club] Type extensionality?, Paolo Herms
Archive powered by MhonArc 2.6.16.