Re: [HoTT] Meta-conjecture about MLTT

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

On 12/09/16 13:47, Thomas Streicher 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.
> 
> This seems to be hard but in my eyes is not the right question. What
> Andrew has shown is that there are definable isomorphic types A and B
> in a universe U and a predicate P on this universe where P(A) is
> inhabited but P(B)° isnot. Actually, this argument is generic since
> one may take P(X)  = IdU;A,X).
> 
> It's like in programming language semantics. One thing is to
> distinguish by maps to 2 and another is to distinguis by maps to \Sigma.
> Inhabited plays the role of \top and not inhabited plays the role of \bot.
> 
> Thomas
> 

Thanks to all who contributed to the discussion (in the list and
off-list - but the off-list remarks made it in to the list independently
by other contributors).

My formulation of the question was ambiguous, with different answers
depending on how we make it precise, and with an unknown answer for one
particular way of making it precise.

Best,
Martin