The Coq mailing list

[Peter LeFanu Lumsdaine <p.l.lumsdaine AT gmail.com>]

>> On Wednesday 30 March 2011 07:13:22 David Baelde wrote:
>>
>>> […] can we prove from inside Coq that any
>>> function of type (forall A:Type, A ->  bool) is extensively equal to
>>> some constant function?

> Daniel Schepler wrote:
>>
>> No, if you add
>>   Axiom classic_dec: forall P:Prop, {P} + {~P}.
>> then you can define
>>   Definition inhabited_bool (A:Type) : bool :=
>>     if classic_dec (inhabited A) then true else false.

On Wed, Mar 30, 2011 at 2:43 PM, Adam Chlipala 
<adam AT chlipala.net>
 wrote:
>
> Is this function really a counterexample?  It doesn't include the argument
> of type [A] from the original question.

Once one has the decidability axiom, one can certainly find plenty of
counterexamples; for instance, the function defined as “the identity
on bool, or the constantly true function on any other type”:

Axiom classic_dec: forall P:Prop, {P} + {~P}.

Definition non_parametric : forall A:Type, A -> bool.
intros A.
case (classic_dec (A = bool)) as [ A_eq_bool | A_neq_bool ].
  (* case A = bool *)
  intros x.  rewrite A_eq_bool in x.  exact x.
  (* case A <> bool *)
  intros x.  exact true.
Defined.

So again, if the decidability axiom is consistent (and as I
understand, it is generally believed to be) then parametricity is not
provable.

–Peter.