The Coq mailing list

[Chad E Brown <cebrown2323 AT yahoo.com>]

Hi Xinyu, and all,

The axiom as you gave it is inconsistent with Coq.  A proof is below.  Maybe you meant something else?

Axiom pa : forall (F : Type -> Type) (f g : forall t, F t) (t : Type), f t = g t -> f = g.

Definition f_ (X : Type) : Type := X -> False.
Definition g_ (X : Type) : Type := False -> X.

Goal False.
cut (f_ = g_). intros e.
cut (g_ True). rewrite <- e. auto.
unfold g_. auto.
apply (pa (fun X => Type) f_ g_ False).
auto.
Qed.

- Chad

---

From: Xinyu Jiang <xj27 AT pantheon.yale.edu>
To: coq-club AT inria.fr
Sent: Wed, September 22, 2010 4:22:11 PM
Subject: [Coq-Club] An axiom about parametricity

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.