The Coq mailing list

[Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>]

On 03/11/2021 16:38, Grant Jurgensen wrote:
> I was wondering if the following property is provable (or disprovable)
> in Coq:
> 
> Theorem forall_eq_elim: forall (A: Type) (B C: A -> Type),
>   (forall a, B a) = (forall a, C a) ->
>   (forall a, B a = C a).
> 
> This is the converse of `forall_extensionality`, found in the standard
> module `Coq.Logic.FunctionalExtensionality`. Assuming functional
> extensionality, this `forall_eq_elim` property essentially states the
> injectivity of the forall binder.

I don't think it's disprovable because you have basically zero way to
prove an equality on types in CIC apart from reflexivity. But as soon as
you have a bit of power over equality this is dead wrong.

Take A := nat, B := fun _ => nat and C := fun _ => bool. By a
cardinality argument, (nat -> bool) = (nat -> nat) but there is no way
that bool = nat. The cardinality argument holds in quite a few models,
e.g. this is true both in Set and in HoTT.

If you pick a model where types are represented as syntactic codes it
might become provable but even there I am not sure.

PMP

Attachment: OpenPGP_signature
Description: OpenPGP digital signature