From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.28.209.203 with SMTP id i194mr957566wmg.4.1473684470131; Mon, 12 Sep 2016 05:47:50 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.25.160.129 with SMTP id j123ls442245lfe.0.gmail; Mon, 12 Sep 2016 05:47:49 -0700 (PDT) X-Received: by 10.25.78.12 with SMTP id c12mr2554300lfb.1.1473684469198; Mon, 12 Sep 2016 05:47:49 -0700 (PDT) Return-Path: Received: from lnx500.hrz.tu-darmstadt.de (mail-relay14.hrz.tu-darmstadt.de. [130.83.156.238]) by gmr-mx.google.com with ESMTPS id 82si711635wmg.3.2016.09.12.05.47.49 for (version=TLS1 cipher=AES128-SHA bits=128/128); Mon, 12 Sep 2016 05:47:49 -0700 (PDT) Received-SPF: pass (google.com: best guess record for domain of stre...@mathematik.tu-darmstadt.de designates 130.83.156.238 as permitted sender) client-ip=130.83.156.238; Authentication-Results: gmr-mx.google.com; spf=pass (google.com: best guess record for domain of stre...@mathematik.tu-darmstadt.de designates 130.83.156.238 as permitted sender) smtp.mailfrom=stre...@mathematik.tu-darmstadt.de Received: from fb04281.mathematik.tu-darmstadt.de (fb04281.mathematik.tu-darmstadt.de [130.83.2.21]) by lnx500.hrz.tu-darmstadt.de (8.14.4/8.14.4/HRZ/PMX) with ESMTP id u8CCllOU005580; Mon, 12 Sep 2016 14:47:48 +0200 (envelope-from stre...@mathematik.tu-darmstadt.de) Received: from fb04209.mathematik.tu-darmstadt.de (fb04209.mathematik.tu-darmstadt.de [130.83.2.209]) by fb04281.mathematik.tu-darmstadt.de (8.12.3/8.12.3/Debian-7.2) with ESMTP id u8CCll70009757; Mon, 12 Sep 2016 14:47:47 +0200 Received: by fb04209.mathematik.tu-darmstadt.de (Postfix, from userid 11003) id 7973F1A5675; Mon, 12 Sep 2016 14:47:47 +0200 (CEST) Date: Mon, 12 Sep 2016 14:47:47 +0200 From: Thomas Streicher To: Martin Escardo Cc: "HomotopyT...@googlegroups.com" Subject: Re: [HoTT] Meta-conjecture about MLTT Message-ID: <20160912124747.GC15456@mathematik.tu-darmstadt.de> References: <5fb00299-f5c6-c63c-aade-a688ba2e5f4b@googlemail.com> MIME-Version: 1.0 Content-Type: text/plain; charset=iso-8859-1 Content-Disposition: inline Content-Transfer-Encoding: 8bit In-Reply-To: <5fb00299-f5c6-c63c-aade-a688ba2e5f4b@googlemail.com> User-Agent: Mutt/1.5.23 (2014-03-12) X-PMX-TU: seen v1.2 by 5.6.1.2065439, Antispam-Engine: 2.7.2.376379, Antispam-Data: 2016.9.12.124217 X-PMX-RELAY: outgoing > 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