From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.129.71.87 with SMTP id u84mr22152943ywa.162.1493958693187; Thu, 04 May 2017 21:31:33 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.157.56.90 with SMTP id r26ls3203924otd.0.gmail; Thu, 04 May 2017 21:31:32 -0700 (PDT) X-Received: by 10.129.154.8 with SMTP id r8mr1538200ywg.133.1493958692914; Thu, 04 May 2017 21:31:32 -0700 (PDT) Received: by 10.55.77.129 with SMTP id a123msqkb; Wed, 3 May 2017 08:04:20 -0700 (PDT) X-Received: by 10.25.79.91 with SMTP id a27mr3419416lfk.27.1493823860500; Wed, 03 May 2017 08:04:20 -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 t10si75850wmb.0.2017.05.03.08.04.20 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 03 May 2017 08:04:20 -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 1d5vpE-00055S-NK; Wed, 03 May 2017 16:04:20 +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 1d5vpE-0003ZS-DR using interface auth-smtp.bham.ac.uk; Wed, 03 May 2017 16:04:20 +0100 Subject: Re: [HoTT] Does MLTT have "or"? To: stre...@mathematik.tu-darmstadt.de References: <20170503105509.GB12588@mathematik.tu-darmstadt.de> <20170503144850.GE24201@mathematik.tu-darmstadt.de> Cc: "HomotopyT...@googlegroups.com" From: Martin Escardo Message-ID: <91d6e594-a961-c580-128b-5c2fbb70732f@googlemail.com> Date: Wed, 3 May 2017 16:04:19 +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: <20170503144850.GE24201@mathematik.tu-darmstadt.de> Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: 7bit 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 15:48, stre...@mathematik.tu-darmstadt.de wrote: >> What you are saying is that there is model where general propositional >> truncations don't exist, but "or" does. Right? > > yes > >> How difficult is to get a model where "or" doesn't exist either? > > depends on what "or" is! in my model Prop has or by impredicativity > but this or doen't coincide with sums on the level of types. I specified what "or" is in point (2) of the initial message of this thread: (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.) Here "proposition" means "type in which any two points are Id-equal". Martin