From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.28.198.133 with SMTP id w127mr1688216wmf.3.1473685282380; Mon, 12 Sep 2016 06:01:22 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.28.46.72 with SMTP id u69ls1343132wmu.8.gmail; Mon, 12 Sep 2016 06:01:21 -0700 (PDT) X-Received: by 10.28.207.131 with SMTP id f125mr1694888wmg.4.1473685281316; Mon, 12 Sep 2016 06:01:21 -0700 (PDT) Return-Path: Received: from sun60.bham.ac.uk (sun60.bham.ac.uk. [147.188.128.137]) by gmr-mx.google.com with ESMTPS id b1si10384wmg.0.2016.09.12.06.01.21 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 12 Sep 2016 06:01:21 -0700 (PDT) Received-SPF: softfail (google.com: domain of transitioning escardo...@googlemail.com does not designate 147.188.128.137 as permitted sender) client-ip=147.188.128.137; Authentication-Results: gmr-mx.google.com; spf=softfail (google.com: domain of transitioning escardo...@googlemail.com does not designate 147.188.128.137 as permitted sender) smtp.mailfrom=escardo...@googlemail.com; dmarc=fail (p=QUARANTINE dis=QUARANTINE) header.from=googlemail.com Received: from [147.188.128.127] (helo=bham.ac.uk) by sun60.bham.ac.uk with esmtp (Exim 4.84) (envelope-from ) id 1bjQrR-0005JQ-Ma; Mon, 12 Sep 2016 14:01:21 +0100 Received: from mx1.cs.bham.ac.uk ([147.188.192.53]) by bham.ac.uk (envelope-from ) with esmtp (Exim 4.84) id 1bjQrQ-0005kE-Fz using interface smart1.bham.ac.uk; Mon, 12 Sep 2016 14:01:20 +0100 Received: from dynamic200-118.cs.bham.ac.uk ([147.188.200.118]) by mx1.cs.bham.ac.uk with esmtp (Exim 4.51) id 1bjQrQ-0008Md-88; Mon, 12 Sep 2016 14:01:20 +0100 Subject: Re: [HoTT] Meta-conjecture about MLTT To: Thomas Streicher References: <5fb00299-f5c6-c63c-aade-a688ba2e5f4b@googlemail.com> <20160912124747.GC15456@mathematik.tu-darmstadt.de> Cc: "HomotopyT...@googlegroups.com" From: Martin Escardo Message-ID: Date: Mon, 12 Sep 2016 14:01:28 +0100 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.2.0 MIME-Version: 1.0 In-Reply-To: <20160912124747.GC15456@mathematik.tu-darmstadt.de> Content-Type: text/plain; charset=windows-1252 Content-Transfer-Encoding: 8bit X-BHAM-SendViaRouter: yes 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