From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.31.136.71 with SMTP id k68mr12244208vkd.8.1493751922314; Tue, 02 May 2017 12:05:22 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.157.7.227 with SMTP id 90ls1742036oto.31.gmail; Tue, 02 May 2017 12:05:21 -0700 (PDT) X-Received: by 10.13.221.202 with SMTP id g193mr1299317ywe.130.1493751921773; Tue, 02 May 2017 12:05:21 -0700 (PDT) Return-Path: Received: from mail-yw0-x22a.google.com (mail-yw0-x22a.google.com. [2607:f8b0:4002:c05::22a]) by gmr-mx.google.com with ESMTPS id n185si229877ywb.3.2017.05.02.12.05.21 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Tue, 02 May 2017 12:05:21 -0700 (PDT) Received-SPF: neutral (google.com: 2607:f8b0:4002:c05::22a is neither permitted nor denied by domain of shu...@sandiego.edu) client-ip=2607:f8b0:4002:c05::22a; Authentication-Results: gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com; spf=neutral (google.com: 2607:f8b0:4002:c05::22a is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Received: by mail-yw0-x22a.google.com with SMTP id l18so74728292ywh.3 for ; Tue, 02 May 2017 12:05:21 -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=zWljJlb3iFxi4/tpXUhDUWjYlnZTbArZmmjIzJASW+8=; b=MWORn0M4+8VHXQVoS0nmMyQ2jhyhZe/pEKZ4dmWf9wT6qDksFTf70+stC4AU05Jtji lJUE4i17/s1lwItEQ9f/Fjf/O6Zc2foBAdmh9HaQxfPPWCpC2bM0EK8NpW4dcb2a08/t KC0fzlBZq8NfUlews4XhEHkc6ZWQ1HEvukkAg31gAcgLCHrFELQn3eRTUCUdoz9Ric6I 9rt5kwYk0/hyQfF5KAmYn/z15cFwdj/GW/urcqOtqJo4KF1s0GKoSYzOueXBAJexAT3v 1Vdz0JNYORVSiYTGLf9VUfy6kKeM2MZHOqhlZR4GGgVyZC1EfW44YuOnSid2s9+CBn2w gheQ== X-Gm-Message-State: AN3rC/4DPlsg632jIBl28qc2YFNkaUFUDvyaFvJ2j/cNrx3fxz916YK/ WgWjgKu6K38uItqnmXU= X-Received: by 10.129.121.197 with SMTP id u188mr27836058ywc.288.1493751921172; Tue, 02 May 2017 12:05:21 -0700 (PDT) Return-Path: Received: from mail-yw0-f181.google.com (mail-yw0-f181.google.com. [209.85.161.181]) by smtp.gmail.com with ESMTPSA id x200sm8159883ywx.72.2017.05.02.12.05.20 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Tue, 02 May 2017 12:05:20 -0700 (PDT) Received: by mail-yw0-f181.google.com with SMTP id k11so74516749ywb.1 for ; Tue, 02 May 2017 12:05:20 -0700 (PDT) X-Received: by 10.129.55.87 with SMTP id e84mr29515893ywa.58.1493751920180; Tue, 02 May 2017 12:05:20 -0700 (PDT) MIME-Version: 1.0 Received: by 10.37.207.1 with HTTP; Tue, 2 May 2017 12:04:59 -0700 (PDT) In-Reply-To: References: From: Michael Shulman Date: Tue, 2 May 2017 12:04:59 -0700 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] Does MLTT have "or"? To: Martin Escardo Cc: "HomotopyT...@googlegroups.com" Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable Some thoughts: - If in addition to function extensionality and propositional extensionality we assume propositional resizing, then ||-|| is constructible using the standard argument that an elementary topos is a regular category. - A model of MLTT with function extensionality but no universes is given by any locally cartesian closed category (perhaps with coproducts if we have binary sum types). It seems that surely not every lccc with coproducts is a regular category -- though I don't have an example ready to hand, let alone an example that also has universes. On Tue, May 2, 2017 at 2:09 AM, 'Martin Escardo' via Homotopy Type Theory 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.