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