From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.13.228.66 with SMTP id n63mr13680036ywe.57.1473631713039; Sun, 11 Sep 2016 15:08:33 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.157.21.49 with SMTP id u46ls1095779otf.43.gmail; Sun, 11 Sep 2016 15:08:32 -0700 (PDT) X-Received: by 10.129.84.69 with SMTP id i66mr13039812ywb.29.1473631712431; Sun, 11 Sep 2016 15:08:32 -0700 (PDT) Return-Path:
In MLTT with equality reflection, we cannot distinguish isomorphic = types.
There was some agreement regarding this in previous discussions here in thi= s list in the past (I think).
But I don't think we actually saw a proof (have we?). As far as I under= stand, we only saw that natural attempts to distinguish examples of isomorp= hic types fail. There was some invokation of realizability models to try to= justify this. But I am not (yet) convinced by the arguments I have seen so= far.
Nevertheless, I am convinced that equality reflection in MLTT cannot be use= d to distinguish any particular pair of isomorphic types. (Prove me wrong.)=
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 does= n't, or to show that this is impossible.
I am strongly inclined to think that this is impossible: that so-called ext= ensional MLTT cannot distinguish isomorphic types.
In particular, equality-reflection has nothing whatsoever to do 5with eleme= ntwise equality.
Of course, what makes this difficult is that MLTT with equality reflection = is inconsistent with univalence.
Martin
--
You received this message because you are subscribed to the Google Groups &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to HomotopyTypeTheory+unsubscribe@googlegroups.com .
For more options, visit https://groups.google.com/d/optout= a>.