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.
What do you mean by a "property", exactly?
There’s also a difference in what you mean by a “type”, which is I think the key difference between the argument I gave, and Andrew’s counterexample (and others’).
The counterexamples show that there can be properties of *small* types, i.e. type families [ X : U |— P(X) Type ], which can distinguish isomorphic (small) types.
The construction I described shows that no property of *all* types — i.e. no type [ . |— P(X) Type ], where X is a new base type, so any closed type can be substituted for X — can distinguish isomorphic types.