From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.237.36.26 with SMTP id r26mr16294900qtc.37.1493814303875; Wed, 03 May 2017 05:25:03 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.107.27.143 with SMTP id b137ls1207832iob.2.gmail; Wed, 03 May 2017 05:25:02 -0700 (PDT) X-Received: by 10.107.171.65 with SMTP id u62mr16777962ioe.0.1493814302902; Wed, 03 May 2017 05:25:02 -0700 (PDT) Return-Path: Received: from mail-yb0-x231.google.com (mail-yb0-x231.google.com. [2607:f8b0:4002:c09::231]) by gmr-mx.google.com with ESMTPS id u66si44634ywg.0.2017.05.03.05.25.02 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 03 May 2017 05:25:02 -0700 (PDT) Received-SPF: neutral (google.com: 2607:f8b0:4002:c09::231 is neither permitted nor denied by domain of shu...@sandiego.edu) client-ip=2607:f8b0:4002:c09::231; Authentication-Results: gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com; spf=neutral (google.com: 2607:f8b0:4002:c09::231 is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Received: by mail-yb0-x231.google.com with SMTP id j17so15536216ybj.0 for ; Wed, 03 May 2017 05:25:02 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=sandiego-edu.20150623.gappssmtp.com; s=20150623; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-transfer-encoding; bh=jRRzSruerFzOSMB2J1diXr1oeaoKGmnKc1iv4Zk067s=; b=oHV8Sao4Xk4po6iYg3sbO30CmrDzpYzZwJaSCt5sSShzjnmIClU1UexsxPS39DxI17 g2B+i0cDWk22YNnLZnBJ5z+cfBc7GXcvR2Fmk8kT7CxEheVT/NVuWeq1Z9zT0ncvgEQx CWSky/Xh3yiZeyKxeazQel1Vhn9gXaXp8qe9qszVfKCyGU+X5XQ7clnOwreeMT/Y4VUH NPmceSo+CYy4VFCpsa915OS5ml0klinYwiQ57/vCp+uMeAk2ecxNb4HQnfxMAswWhSoZ KRkqM3ymhFpfUVKj3jDnum1D5kCWFgmTsqlFpMVcMG1hu7W8dtR/b9DTbBdrg8L9OSNN GnyQ== X-Gm-Message-State: AN3rC/6N6uALEqc7QipevqCnLyQvzD6tYu8WvgowMhvBFvd+VFzkqyS5 mdw0/WVbfm3/mT6CVP4= X-Received: by 10.37.41.130 with SMTP id p124mr30306014ybp.24.1493814302426; Wed, 03 May 2017 05:25:02 -0700 (PDT) Return-Path: Received: from mail-yw0-f169.google.com (mail-yw0-f169.google.com. [209.85.161.169]) by smtp.gmail.com with ESMTPSA id d2sm5791054ywe.64.2017.05.03.05.25.01 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 03 May 2017 05:25:01 -0700 (PDT) Received: by mail-yw0-f169.google.com with SMTP id 203so83652905ywe.0 for ; Wed, 03 May 2017 05:25:01 -0700 (PDT) X-Received: by 10.129.145.133 with SMTP id i127mr5561182ywg.229.1493814301535; Wed, 03 May 2017 05:25:01 -0700 (PDT) MIME-Version: 1.0 Received: by 10.37.207.1 with HTTP; Wed, 3 May 2017 05:24:41 -0700 (PDT) In-Reply-To: <0972e3bc-7d2c-46ae-a644-a94ede4e8724@googlegroups.com> References: <0972e3bc-7d2c-46ae-a644-a94ede4e8724@googlegroups.com> From: Michael Shulman Date: Wed, 3 May 2017 05:24:41 -0700 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] Re: Does MLTT have "or"? To: Andrew Polonsky Cc: Homotopy Type Theory Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable Note that the "un-resized" impredicative truncation and disjunction, in addition to living in a larger universe themselves, only have the appropriate universal property with respect to propositions in the *smaller* universe. On Wed, May 3, 2017 at 5:17 AM, Andrew Polonsky wrote: > If you don't mind the proposition living in a higher universe, then > certainly the impredicative encoding will do: > > P\/Q :=3D =E2=88=8F(X:U) isProp(X) -> (P -> X) -> (Q -> X) -> X > > 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 :=3D ||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) :=3D =CE=A3(X':U), >> isProp(X') >> =C3=97 (X=E2=86=92X') >> =C3=97 =CE=A0(P:U), (isProp(P) =C3=97 (X=E2=86= =92P)) =E2=86=92 (X'=E2=86=92P). >> >> 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.