The Coq mailing list

[Thorsten Altenkirch <txa AT Cs.Nott.AC.UK>]

On 23 Sep 2010, at 21:23, Taral wrote:

> On Wed, Sep 22, 2010 at 6:55 AM, Xinyu Jiang 
>Â <xj27 AT pantheon.yale.edu>
>  wrote:
>> Hi all,
>> I would like to add an axiom somehow like:
>> 
>> "forall (F : Type -> Type) (f g : forall t, F t) (t : Type), f t = g t ->
>> f = g"
> 
> That's not parametricity. This kind of is:
> 
> forall (F : Type -> Type) (f g : forall t, F t), (forall (t : Type), f
> t = g t) -> f = g.

Isn't this just extensionality?

T.

> 
> -- 
> Taral 
>Â <taralx AT gmail.com>
> "Please let me know if there's any further trouble I can give you."
>  -- Unknown
>