The Coq mailing list

[Xinyu Jiang <xj27 AT pantheon.yale.edu>]

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.