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?

If you mean a type family, e.g.,

X : U |- P(X) : Type

then a counterexample is

A = Nat x Bool

B = Bool x Nat

P(X) = Id(U;X,A)

Cheers,

Andrew