The Coq mailing list

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

On 03/11/2021 18:23, Grant Jurgensen wrote:
> I was under the impression that equality only followed from cardinality
> in HoTT.

That's true for hSets but it breaks when you have higher structure.

> 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?

Ironically, types in type theory are very amorphous. They just need to
classify the kind of objects you're talking about and that's it. Since
you have essentially no way to inspect them in CIC there is a lot of
moving parts in the semantics of types, especially regarding equality.

A syntactic equality on types would indeed prove that the two above
types are distinct. Since my last post I convinced myself that if you
pick the types-as-codes model (i.e. Type is represented by a
inductive-recursive definition encoding the possible type former) then
your theorem holds. Indeed, in the model

(forall x : A, B) := code_pi A (fun x => B)

so you get injectivity of type formers by no-confusion of constructors.
But this is a very, very specific model that also induces a lot of
properties you probably don't want, e.g. it utterly destroys
parametricity. You can now inspect an abstract type at runtime and do
things by case analysis on its shape.

> 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.

I don't think that there is anything philosophical in this discussion,
it's a matter of (programming) language design. If you live in a
univalent world, you have a lot of invariants that come for free but you
are more constrained. If you live in the types-as-codes world, you now
got a dependently-typed variant of (a better behaved) Python.

PMP

Attachment: OpenPGP_signature
Description: OpenPGP digital signature