From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.99.1.138 with SMTP id 132mr404938pgb.162.1493958693247; Thu, 04 May 2017 21:31:33 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.157.82.106 with SMTP id q42ls3253133otg.12.gmail; Thu, 04 May 2017 21:31:32 -0700 (PDT) X-Received: by 10.13.238.65 with SMTP id x62mr18763129ywe.5.1493958692916; Thu, 04 May 2017 21:31:32 -0700 (PDT) Received: by 10.55.11.5 with SMTP id 5msqkl; Wed, 3 May 2017 05:24:26 -0700 (PDT) X-Received: by 10.46.83.12 with SMTP id h12mr3959900ljb.24.1493814265880; Wed, 03 May 2017 05:24:25 -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 w126si24026wmd.1.2017.05.03.05.24.25 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 03 May 2017 05:24:25 -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.54] (helo=mailer3) by sun60.bham.ac.uk with esmtp (Exim 4.84) (envelope-from ) id 1d5tKT-0006u2-OK for HomotopyT...@googlegroups.com; Wed, 03 May 2017 13:24:25 +0100 Received: from [31.185.238.126] (helo=[192.168.1.75]) by bham.ac.uk (envelope-from ) with esmtpsa (TLSv1.2:DHE-RSA-AES128-SHA:128) (Exim 4.84) id 1d5tKT-0007yC-ER for HomotopyT...@googlegroups.com using interface auth-smtp.bham.ac.uk; Wed, 03 May 2017 13:24:25 +0100 Subject: Re: [HoTT] Re: Does MLTT have "or"? To: Homotopy Type Theory References: <0972e3bc-7d2c-46ae-a644-a94ede4e8724@googlegroups.com> From: Martin Escardo Message-ID: <6faa4dba-b6ed-752e-6877-81f77d20ddde@googlemail.com> Date: Wed, 3 May 2017 13:24:25 +0100 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.8.0 MIME-Version: 1.0 In-Reply-To: <0972e3bc-7d2c-46ae-a644-a94ede4e8724@googlegroups.com> Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: 8bit X-BHAM-SendViaRouter: yes X-BHAM-AUTH-data: TLSv1.2:DHE-RSA-AES128-SHA:128 via 147.188.128.21:465 (escardom) On 03/05/17 13:17, andrew....@gmail.com wrote: > If you don't mind the proposition living in a higher universe, then > certainly the impredicative encoding will do: > > P\/Q := ∏(X:U) isProp(X) -> (P -> X) -> (Q -> X) -> X Assuming funext to show that this is indeed a proposition. This is equivalent to the large truncation of P+Q discussed in my previous message. As I said, if a small truncation exists, it is equivalent to the large truncation, which always exists for any type, assuming funext. Martin > > satisfies > > P -> P\/Q > Q -> P\/Q > isProp(R) -> (P->R) -> (Q->R) -> (P\/Q -> R) > > Best, > Andrew > > On Tuesday, May 2, 2017 at 12:45:41 PM UTC-4, Martin Hotzel Escardo wrote: > > 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 > > -- > You received this message because you are subscribed to the Google > Groups "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send > an email to HomotopyTypeThe...@googlegroups.com > . > For more options, visit https://groups.google.com/d/optout.