The Coq mailing list

["Grant Jurgensen" <mailing-lists.coq AT grant.jurgensen.dev>]

I was under the impression that equality only followed from cardinality in HoTT. Wouldn't a more "traditional" view on type equality identify types with their inhabitants, and therefore suggest `nat -> bool` and `nat -> nat` to be unequal? Or am I misunderstanding something?

Still, I take your point that type equality is quite under-specified in CIC and therefore open to many possible models and interpretation. I'm not sure its worth adding any fact axiomatically unless one is prepared to take a strong philosophical stance on the meaning of type equality.

Thanks,

Grant

On Wed, Nov 3, 2021, at 12:03 PM, Pierre-Marie Pédrot wrote:

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

Attachments:

• OpenPGP_signature