From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.25.15.103 with SMTP id e100mr69733lfi.16.1494755657194; Sun, 14 May 2017 02:54:17 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.25.228.212 with SMTP id x81ls428041lfi.1.gmail; Sun, 14 May 2017 02:54:15 -0700 (PDT) X-Received: by 10.25.195.146 with SMTP id t140mr66296lff.13.1494755655376; Sun, 14 May 2017 02:54:15 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1494755655; cv=none; d=google.com; s=arc-20160816; b=myYA/pSdMQCxTUqW9GmIh5DvEDDAtcNhkuW3INL2ZtMWdtRWUXWoVprF/VSFk5FIIC wggTcadSmPjjmiZRJPBUF7t9442hmhbfsr9DccpB9Q50vBmNSQkLbUdhvUCnQpXgxGR8 LhyBn4DBjf4APhAyEe+WBm7E5R+SaAcxDHSTVej07Y/1po+GgDta1aH4miX4qsm0QhwD 3CukdRUa58MPBr7AIo4bBW2/HyBd0eTUdmdvNzFIuPsj07uRMyHfWAbEQuVh9Xb8TUeC kfOfO2vtFU7y7ackH0akt9P/vw3hXyZi2JUe95VkL6bmk+ayzeafvkek/4tuYYbqsLGQ of4g== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=importance:content-transfer-encoding:mime-version:user-agent:cc:to :from:subject:date:references:in-reply-to:message-id :arc-authentication-results; bh=9BkCjdrIzcNJI86N3h37sjkzvd1SWnb1xKtZaD91pN8=; b=SOwJFt9rryTVViP4a1OCnBACwfXqe2MQetaAKbuzo1DQheZsmkDJgSdQKHIVcNPVAC FOi51YTb3b3WUfrE2lN/mU2CO9fgtUTwePK5fzIzuy/AdfHXG2Xl7orc9a0BLhbqqpub Rs2g+DVRgzttl4vu+oSA0SbQEh6DYLQHbqDcodbbpLvLCvnMUsckLf45Zg+QYNyHgFag 9YdHdLJ4APdajlgkqBbrjhZqjWLayvhREsvppRUz+/0nbv9wRdKyAYRSNidsHz0848pb OoM4BaYHKpZA5XH0hxkXMqdIo+5xnwQk8vAbsKaC7acSbZLZX6/t2uVoGH7SACcIQKPq zYRw== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=pass (google.com: best guess record for domain of stre...@mathematik.tu-darmstadt.de designates 130.83.156.225 as permitted sender) smtp.mailfrom=stre...@mathematik.tu-darmstadt.de Return-Path: Received: from lnx500.hrz.tu-darmstadt.de (lnx500.hrz.tu-darmstadt.de. [130.83.156.225]) by gmr-mx.google.com with ESMTPS id q200si471944wme.2.2017.05.14.02.54.15 for (version=TLS1 cipher=AES128-SHA bits=128/128); Sun, 14 May 2017 02:54:15 -0700 (PDT) Received-SPF: pass (google.com: best guess record for domain of stre...@mathematik.tu-darmstadt.de designates 130.83.156.225 as permitted sender) client-ip=130.83.156.225; 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.225 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 lnx500.hrz.tu-darmstadt.de (8.14.4/8.14.4/HRZ/PMX) with ESMTP id v4E9rXTn019912; Sun, 14 May 2017 11:53:33 +0200 (envelope-from stre...@mathematik.tu-darmstadt.de) Received: from webmail.mathematik.tu-darmstadt.de (fb04277.mathematik.tu-darmstadt.de [130.83.2.17]) by fb04281.mathematik.tu-darmstadt.de (8.12.3/8.12.3/Debian-7.2) with ESMTP id v4E9sDES025571; Sun, 14 May 2017 11:54:13 +0200 Received: from 93.220.247.97 (SquirrelMail authenticated user streicher) by webmail.mathematik.tu-darmstadt.de with HTTP; Sun, 14 May 2017 11:54:13 +0200 Message-ID: In-Reply-To: References: <1cef3819-ed3f-c684-d070-f49576045a19@googlemail.com> Date: Sun, 14 May 2017 11:54:13 +0200 Subject: Re: [HoTT] Does MLTT have "or"? From: stre...@mathematik.tu-darmstadt.de To: "Michael Shulman" Cc: "Martin Escardo" , "HomotopyT...@googlegroups.com" User-Agent: SquirrelMail/1.4.21 MIME-Version: 1.0 Content-Type: text/plain;charset=iso-8859-1 Content-Transfer-Encoding: 8bit X-Priority: 3 (Normal) Importance: Normal X-PMX-TU: seen v1.2 by 5.6.1.2065439, Antispam-Engine: 2.7.2.376379, Antispam-Data: 2017.5.14.94516 X-PMX-RELAY: outgoing The question is not one of universal properties but of existence. I wo der whether every posetal lccc has binary sups. Every cartesian closd poset is lccc but need not have binary sups, e.g. the free ccc over 1 generator is lccc but has no binary sums. Thomas