Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] An axiom about parametricity

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] An axiom about parametricity


chronological Thread 
  • From: Taral <taralx AT gmail.com>
  • To: Xinyu Jiang <xj27 AT pantheon.yale.edu>
  • Cc: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] An axiom about parametricity
  • Date: Thu, 23 Sep 2010 13:23:09 -0700
  • Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-type:content-transfer-encoding; b=rr3X7PtvWGrVWNJa1HPj7yxdL+lKndK9wPweg3xBbeiTlMs0G7OBKieSZsWQAHG9L4 PQ8tWzkeIZtDPlqVVpBgE9oBvF68eJ9OnQl+5Mn4XWa2/qtcQ/k4il+DpGwUQWoWFUVb jMLZmi4KF1HfRjEzBI0ZWyTwCU6FujHq8lWWU=
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.

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


Archive powered by MhonArc 2.6.16.

Top of Page