From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.200.41.47 with SMTP id y44mr20264174qty.51.1493958693289; Thu, 04 May 2017 21:31:33 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.157.44.10 with SMTP id f10ls2865711otb.46.gmail; Thu, 04 May 2017 21:31:33 -0700 (PDT) X-Received: by 10.157.39.13 with SMTP id r13mr20723256ota.118.1493958693013; Thu, 04 May 2017 21:31:33 -0700 (PDT) Received: by 10.55.98.205 with SMTP id w196msqkb; Wed, 3 May 2017 07:25:48 -0700 (PDT) X-Received: by 10.28.6.198 with SMTP id 189mr445635wmg.0.1493821548245; Wed, 03 May 2017 07:25:48 -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 n197si57373wmg.3.2017.05.03.07.25.48 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 03 May 2017 07:25:48 -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 1d5vDv-00024J-PW; Wed, 03 May 2017 15:25:47 +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 1d5vDv-0008Um-Ff using interface auth-smtp.bham.ac.uk; Wed, 03 May 2017 15:25:47 +0100 Subject: Re: [HoTT] Does MLTT have "or"? To: stre...@mathematik.tu-darmstadt.de References: <20170503105509.GB12588@mathematik.tu-darmstadt.de> Cc: "HomotopyT...@googlegroups.com" From: Martin Escardo Message-ID: Date: Wed, 3 May 2017 15:25:47 +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: <20170503105509.GB12588@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 11:55, stre...@mathematik.tu-darmstadt.de wrote: >> (4) What is a model of intensional MLTT with a universe such that >> ||-|| doesn't exist? > > In my 1992 TCS paper I have constructed an impredicative universe > within Asm(K_1) (separated objects of effective topos) which is not > reflective. The universe consists of all powers of N together with the > initial object. All its elements are empty or contain infinitely many > global elements. > > But or is definable `a la Russel-Prawitz. What you are saying is that there is model where general propositional truncations don't exist, but "or" does. Right? How difficult is to get a model where "or" doesn't exist either? Best, Martin