The Coq mailing list

[Bruno Barras <bruno.barras AT inria.fr>]

On 09/22/2010 05:55 PM, AUGER Cedric wrote:
> Le Wed, 22 Sep 2010 22:22:11 +0800,
> Xinyu 
> Jiang<xj27 AT pantheon.yale.edu>
>   a écrit :
>
> > 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"
> >
> >    to Coq. It seems to be reasonable because of the parametricity of
> > Coq's logic. But I wonder if the axiom is indeed consistent with Coq.
> > If so, would it collide against other axioms like exclusive of the
> > middle? If not, what would the counter example be like? Thanks very
> > much.
>
> Variable Absurd: forall (F : Type ->  Type) (f g : forall t, F t)
>           (t : Type), f t = g t ->  f = g.
>
>
> In fact your axioms states that if "f" and "g" are equal in one point,
> then they are equal; it looks a little like to "proof irrelevance" but
> in "Type".

Right. And it clearly does not hold: True and False are quite different 
types: you can prove True, and if they were equal you could prove False 
by rewriting.

> But I know that axiom-free inhabitants of "Type ->  Type" in Coq are
> constant functions, as matching is not allowed for Type;

No. identity is not a constant function when the domain has at least two 
elements :o)
So (Absurd (fun _=>Type) (fun P => P) (fun _ => False) False
    (@eq_refl Type False))
is a proof of (fun P => P) = (fun _ => False)
(they match on t=False)
Then (fun P=>P) True = (fun _=>False) True by rewriting.
You've deduced True = False.
I leave the proof of False as an exercise.

I don't know what you mean by "parametricity of Coq's logic". It is true 
that you cannot do some case-analysis on objects in Type, but dependent 
types and the complex language on types will not give you the same 
"theorems for free" as for system F...

Bruno Barras.