I suspect "one of them provably has but the other doesn't" should mean "one
of them provably has but the other provably does not have".

On Sun, Sep 11, 2016 at 10:20 PM Andrew Polonsky <andrew....@gmail.com>
wrote:

> 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
>
> --
> You received this message because you are subscribed to the Google Groups
> "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to HomotopyTypeThe...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.
>