From mboxrd@z Thu Jan  1 00:00:00 1970
X-Received: by 10.25.202.94 with SMTP id h30mr998079lfj.2.1493823418977;
        Wed, 03 May 2017 07:56:58 -0700 (PDT)
X-BeenThere: homotopytypetheory@googlegroups.com
Received: by 10.46.69.4 with SMTP id s4ls180174lja.46.gmail; Wed, 03 May 2017
 07:56:57 -0700 (PDT)
X-Received: by 10.46.88.70 with SMTP id x6mr4120871ljd.0.1493823417768;
        Wed, 03 May 2017 07:56:57 -0700 (PDT)
Return-Path: <stre...@mathematik.tu-darmstadt.de>
Received: from lnx141.hrz.tu-darmstadt.de (lnx141.hrz.tu-darmstadt.de. [130.83.156.236])
        by gmr-mx.google.com with ESMTPS id h203si51608wmf.1.2017.05.03.07.56.57
        for <HomotopyT...@googlegroups.com>
        (version=TLS1 cipher=AES128-SHA bits=128/128);
        Wed, 03 May 2017 07:56:57 -0700 (PDT)
Received-SPF: pass (google.com: best guess record for domain of stre...@mathematik.tu-darmstadt.de designates 130.83.156.236 as permitted sender) client-ip=130.83.156.236;
Authentication-Results: gmr-mx.google.com;
       spf=pass (google.com: best guess record for domain of stre...@mathematik.tu-darmstadt.de designates 130.83.156.236 as permitted sender) smtp.mailfrom=stre...@mathematik.tu-darmstadt.de
Received: from lnx503.hrz.tu-darmstadt.de (lnx503.hrz.tu-darmstadt.de [130.83.156.232])
	by lnx141.hrz.tu-darmstadt.de (8.14.4/8.13.8) with ESMTP id v43EpENP029191;
	Wed, 3 May 2017 16:51:23 +0200
	(envelope-from stre...@mathematik.tu-darmstadt.de)
Received: from fb04281.mathematik.tu-darmstadt.de (fb04281.mathematik.tu-darmstadt.de [130.83.2.21])
	by lnx503.hrz.tu-darmstadt.de (8.14.4/8.14.4/HRZ/PMX) with ESMTP id v43EmoI1026783;
	Wed, 3 May 2017 16:48:50 +0200
	(envelope-from stre...@mathematik.tu-darmstadt.de)
Received: from fb04209.mathematik.tu-darmstadt.de (fb04209.mathematik.tu-darmstadt.de [130.83.2.209])
	by fb04281.mathematik.tu-darmstadt.de (8.12.3/8.12.3/Debian-7.2) with ESMTP id v43EmoES030146;
	Wed, 3 May 2017 16:48:50 +0200
Received: by fb04209.mathematik.tu-darmstadt.de (Postfix, from userid 11003)
	id 66F241A3AB7; Wed,  3 May 2017 16:48:50 +0200 (CEST)
Date: Wed, 3 May 2017 16:48:50 +0200
From: Thomas Streicher <stre...@mathematik.tu-darmstadt.de>
To: Martin Escardo <escardo...@googlemail.com>
Cc: "HomotopyT...@googlegroups.com" <HomotopyT...@googlegroups.com>
Subject: Re: [HoTT] Does MLTT have "or"?
Message-ID: <20170503144850.GE24201@mathematik.tu-darmstadt.de>
References: <c0286cfb-2394-8e33-715b-d996dea6ab82@googlemail.com>
 <20170503105509.GB12588@mathematik.tu-darmstadt.de>
 <d43ff886-58d8-29ce-b24e-c74d9a22c93c@googlemail.com>
MIME-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Content-Disposition: inline
In-Reply-To: <d43ff886-58d8-29ce-b24e-c74d9a22c93c@googlemail.com>
User-Agent: Mutt/1.5.23 (2014-03-12)
X-PMX-TU: seen v1.2 by 5.6.1.2065439, Antispam-Engine: 2.7.2.376379, Antispam-Data: 2017.5.3.144215
X-PMX-RELAY: outgoing

> 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.

Thomas