coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] An axiom about parametricity

From: Taral <taralx AT gmail.com>
To: Thorsten Altenkirch <txa AT cs.nott.ac.uk>
Cc: Xinyu Jiang <xj27 AT pantheon.yale.edu>, coq-club AT inria.fr
Subject: Re: [Coq-Club] An axiom about parametricity
Date: Fri, 24 Sep 2010 15:52:53 -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=EZFex+EWer3tT41CoiUwY+x6uPLX/4frjO8kmOX/o+e9x0VTjmaqALap52KbqFkiR0 sh572BDHyVx7ONU7w62dNXBe3q99kVx5bUYvPdUG1ZCX21Cu64eGlJmPA8pJulBOv4Zq li8hecmNbS237fVD8HmJSW22SEsDU+rHPEWR0=

On Fri, Sep 24, 2010 at 6:28 AM, Thorsten Altenkirch
<txa AT cs.nott.ac.uk>
wrote:
>> forall (F : Type -> Type) (f g : forall t, F t), (forall (t : Type), f
>> t = g t) -> f = g.
>
> Isn't this just extensionality?

Yes, it is. Nevermind me, nothing to see here.

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

[Coq-Club] An axiom about parametricity, Xinyu Jiang
- Message not available
  - Message not available
    - [Coq-Club] An axiom about parametricity, Xinyu Jiang
      - Re: [Coq-Club] An axiom about parametricity, Chad E Brown
      - Re: [Coq-Club] An axiom about parametricity, AUGER Cedric
      - Message not available
        
        Re: [Coq-Club] An axiom about parametricity, Bruno Barras
        
        Re: [Coq-Club] An axiom about parametricity, Thorsten Altenkirch
- Message not available
  - Message not available
    - Message not available
      - Re: [Coq-Club] An axiom about parametricity, Arthur Chargu�raud
- Re: [Coq-Club] An axiom about parametricity, Taral
  - Re: [Coq-Club] An axiom about parametricity, Thorsten Altenkirch
    - Re: [Coq-Club] An axiom about parametricity, Taral
- <Possible follow-ups>
- Re: [Coq-Club] An axiom about parametricity, xinyu . jiang