From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.31.129.198 with SMTP id c189mr103501vkd.12.1493743541653; Tue, 02 May 2017 09:45:41 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.157.47.99 with SMTP id h90ls1602552otb.38.gmail; Tue, 02 May 2017 09:45:41 -0700 (PDT) X-Received: by 10.237.49.105 with SMTP id 96mr14763718qtg.18.1493743541038; Tue, 02 May 2017 09:45:41 -0700 (PDT) Received: by 10.55.77.129 with SMTP id a123msqkb; Tue, 2 May 2017 02:02:41 -0700 (PDT) X-Received: by 10.25.199.134 with SMTP id x128mr2614190lff.4.1493715760599; Tue, 02 May 2017 02:02:40 -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 130si49606wmq.0.2017.05.02.02.02.40 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Tue, 02 May 2017 02:02:40 -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 sp=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 1d5Thg-0004cU-NY for HomotopyT...@googlegroups.com; Tue, 02 May 2017 10:02:40 +0100 Received: from mx1.cs.bham.ac.uk ([147.188.192.53]) by bham.ac.uk (envelope-from ) with esmtp (Exim 4.84) id 1d5Thg-00027l-Dj for HomotopyT...@googlegroups.com using interface smart1.bham.ac.uk; Tue, 02 May 2017 10:02:40 +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 1d5Thg-0000dA-6w for HomotopyT...@googlegroups.com; Tue, 02 May 2017 10:02:40 +0100 From: Martin Escardo Subject: Does MLTT have "or"? To: "HomotopyT...@googlegroups.com" Message-ID: Date: Tue, 2 May 2017 10:09:15 +0100 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.8.0 MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: 8bit X-BHAM-SendViaRouter: yes Last week in a meeting I had a technical discussion with somebody, who suggested to post the question here. (1) Prove (internally) or disprove (as a meta-theorem, probably with a counter-model) the following in (intensional) Martin-Loef Type Theory: * The poset of subsingletons (or propositions or truth values) has binary joins (or disjunction). (We know it has binary meets and Heyting implication, which amounts to saying it is a Heyting semilattice. Is it a lattice?) (2) The question is whether given any two propositions P and Q we can find a proposition R with P->R and Q->R such that for any proposition R' with P->R' and Q->R' we have R->R'. (R is the least upper bound of P and Q.) (3) Of course, if MLTT had propositional truncations ||-||, then the answer would be R := ||P+Q||. But we can ask this question for MLTT before we postulate propositional truncations as in (1)-(2). (4) What is a model of intensional MLTT with a universe such that ||-|| doesn't exist? More precisely, define, internally in intensional MLTT, hasTruncation(X:U) := Σ(X':U), isProp(X') × (X→X') × Π(P:U), (isProp(P) × (X→P)) → (X'→P). Is there a model, with universes, the falsifies this? Preferably, we want models that falsify this but validate function extensionality (and perhaps also propositional extensionality). Best, Martin