From mboxrd@z Thu Jan  1 00:00:00 1970
X-Received: by 10.25.223.70 with SMTP id q6mr3258491lfj.6.1493808912081;
        Wed, 03 May 2017 03:55:12 -0700 (PDT)
X-BeenThere: homotopytypetheory@googlegroups.com
Received: by 10.46.88.82 with SMTP id x18ls194729ljd.9.gmail; Wed, 03 May 2017
 03:55:10 -0700 (PDT)
X-Received: by 10.46.5.76 with SMTP id 73mr2982936ljf.26.1493808910823;
        Wed, 03 May 2017 03:55:10 -0700 (PDT)
Return-Path: <stre...@mathematik.tu-darmstadt.de>
Received: from lnx503.hrz.tu-darmstadt.de (mail-relay15.hrz.tu-darmstadt.de. [130.83.156.239])
        by gmr-mx.google.com with ESMTPS id n4si22052wmf.2.2017.05.03.03.55.10
        for <HomotopyT...@googlegroups.com>
        (version=TLS1 cipher=AES128-SHA bits=128/128);
        Wed, 03 May 2017 03:55:10 -0700 (PDT)
Received-SPF: pass (google.com: best guess record for domain of stre...@mathematik.tu-darmstadt.de designates 130.83.156.239 as permitted sender) client-ip=130.83.156.239;
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.239 as permitted sender) smtp.mailfrom=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 v43AtAHt014526;
	Wed, 3 May 2017 12:55:10 +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 v43At9ES025436;
	Wed, 3 May 2017 12:55:09 +0200
Received: by fb04209.mathematik.tu-darmstadt.de (Postfix, from userid 11003)
	id DEA0C1A0B54; Wed,  3 May 2017 12:55:09 +0200 (CEST)
Date: Wed, 3 May 2017 12:55:09 +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: <20170503105509.GB12588@mathematik.tu-darmstadt.de>
References: <c0286cfb-2394-8e33-715b-d996dea6ab82@googlemail.com>
MIME-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Content-Disposition: inline
In-Reply-To: <c0286cfb-2394-8e33-715b-d996dea6ab82@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.104816
X-PMX-RELAY: outgoing

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

Thomas