Meta-conjecture about MLTT

[Martin Escardo <escardo...@googlemail.com>]

In MLTT with equality reflection, we cannot distinguish isomorphic types.

There was some agreement regarding this in previous discussions here in 
this list in the past (I think).

But I don't think we actually saw a proof (have we?). As far as I 
understand, we only saw that natural attempts to distinguish examples of 
isomorphic types fail. There was some invokation of realizability models 
to try to justify this. But I am not (yet) convinced by the arguments I 
have seen so far.

Nevertheless, I am convinced that equality reflection in MLTT cannot be 
used to distinguish any particular pair of isomorphic types. (Prove me 
wrong.)

The meta-task is to either produce two isomorphic types in an empty 
context, together with a property that one of them provably has but the 
other doesn't, or to show that this is impossible.

I am strongly inclined to think that this is impossible: that so-called 
extensional MLTT cannot distinguish isomorphic types.

In particular, equality-reflection has nothing whatsoever to do 5with 
elementwise equality.

Of course, what makes this difficult is that MLTT with equality 
reflection is inconsistent with univalence.


Martin