From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.157.48.51 with SMTP id d48mr4608450otc.27.1494915641306; Mon, 15 May 2017 23:20:41 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.36.118.133 with SMTP id z127ls2481907itb.12.canary-gmail; Mon, 15 May 2017 23:20:40 -0700 (PDT) X-Received: by 10.99.167.79 with SMTP id w15mr4845391pgo.30.1494915640566; Mon, 15 May 2017 23:20:40 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1494915640; cv=none; d=google.com; s=arc-20160816; b=TYELVuRBO+CixMkkk7IiBVm554kKK+lEFcbEol9VSWrGZS5rcwHEyEvpn7PjzddNrT K4ZgnAFBD8INoelYy8Xz9sVed9etViSATHfFFUsZ+V97hmkFQA4KvvoPKAc7i7/KcIyt kL/vnsdBz7UYNG00QCRxL12Rx9AE/P8TQcm/1uheOjzJrIkxOyqTlYR1LX8kgIHc+Kd2 w5WLg/01EQa2r9V1gPRBmmiAL8nnnMNOcVkYnxgvJyjZBWbztpBLJp6x05LX2X/ylExI qB1tdY7BTruvWo2izUdAwp5FdvsE9qz/zDTJcNpGSF8ylWcE5FBo4J7uFhpSgitiu/3F MHuA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=cc:to:subject:message-id:date:from:references:in-reply-to :mime-version:dkim-signature:arc-authentication-results; bh=qkfstQb5xjbDbpN66/ZKjgYt9WJwVuuCaEvW2DpzPyY=; b=TrbXfx8Nap0otuinnW7EyU+NBwWMYBjH8tBoMDlKWXwCsp8ji+t8MU9nS4agYtMv5V IARiGkZoE6VaXWnPaSBkp1wrcngUexWrjZDxCMTZzD2U1VvjiCuNZvOaiK7I8/0r41Kz Bye6RIQYuhfEJZvGS2Pv+kM7E0FLrw5835tVshdOffIhGhI7g39tmjXkT5EQ9AEBEzCQ 46N1Od2oQcLEG9Ue2wWq/RimYL2cxsdNsvb4NiEBHRZiBmkbSZJiKrzv4cNyvs5+7mP0 OZjpDXKgkr5cvamoKxZKV8VGOcRdDJUde8JB2wLwK9M8bmDtFiBUT7SWwwkweXBCd3Ab Mv3w== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com; spf=neutral (google.com: 2607:f8b0:4002:c09::22f is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Return-Path: Received: from mail-yb0-x22f.google.com (mail-yb0-x22f.google.com. [2607:f8b0:4002:c09::22f]) by gmr-mx.google.com with ESMTPS id o66si1431037ywd.7.2017.05.15.23.20.40 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 15 May 2017 23:20:40 -0700 (PDT) Received-SPF: neutral (google.com: 2607:f8b0:4002:c09::22f is neither permitted nor denied by domain of shu...@sandiego.edu) client-ip=2607:f8b0:4002:c09::22f; Authentication-Results: gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com; spf=neutral (google.com: 2607:f8b0:4002:c09::22f is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Received: by mail-yb0-x22f.google.com with SMTP id p143so32956952yba.2 for ; Mon, 15 May 2017 23:20:40 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=sandiego-edu.20150623.gappssmtp.com; s=20150623; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc; bh=qkfstQb5xjbDbpN66/ZKjgYt9WJwVuuCaEvW2DpzPyY=; b=dmTBY7pHiSf2iuAYVuzp7qYSCxsh+qWVqDR9Bf4kNEmPoHTLH9aLwkZ24W22IShDq+ P5h1ppNhAsXdOUf+cZBqthi7tie7frzHu0TQCQ0UNc7vEiYc0PeNdvtrYaTEI2f02HWv SPE0XcxXM/A2R/eMkRE8yHzDlMw6/eQJbQUqqwmYvH7JwaUQ8aFN4PT/raqjTEVRXdfi Nc9+0LF74lqtpJrRosYWjGht9pZGsEEuBg6Nlx64XRxvyjd/zlgX2iNQ73GZj90fsMBm aaLbyc3wgYlLgT/r5naiOJleq5EtMEiwW/dXz9n7ntnWDbNAFdJzpA7CNfCQ3EOeBalW COHA== X-Gm-Message-State: AODbwcC1Mc1YXV44r+MvvjnzFuxb2OqO1Y4v7SvDF56vIJxxGzAnsiZZ z+sUnFdvV5E9SThF9EE= X-Received: by 10.37.70.70 with SMTP id t67mr8395420yba.44.1494915640139; Mon, 15 May 2017 23:20:40 -0700 (PDT) Return-Path: Received: from mail-yw0-f170.google.com (mail-yw0-f170.google.com. [209.85.161.170]) by smtp.gmail.com with ESMTPSA id l12sm6779451ywh.29.2017.05.15.23.20.39 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 15 May 2017 23:20:39 -0700 (PDT) Received: by mail-yw0-f170.google.com with SMTP id 203so48101525ywe.0 for ; Mon, 15 May 2017 23:20:39 -0700 (PDT) X-Received: by 10.129.123.213 with SMTP id w204mr8742752ywc.120.1494915639428; Mon, 15 May 2017 23:20:39 -0700 (PDT) MIME-Version: 1.0 Received: by 10.37.207.1 with HTTP; Mon, 15 May 2017 23:20:19 -0700 (PDT) In-Reply-To: References: <1cef3819-ed3f-c684-d070-f49576045a19@googlemail.com> From: Michael Shulman Date: Mon, 15 May 2017 23:20:19 -0700 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] Does MLTT have "or"? To: Martin Escardo Cc: "HomotopyT...@googlegroups.com" Content-Type: text/plain; charset="UTF-8" On Sat, May 13, 2017 at 2:46 PM, Michael Shulman wrote: > 3. A Boolean coherent category automatically has a subobject > classifier, namely 1+1. Thus, if it is also cartesian closed, it is > automatically a topos. I should have said, a Boolean *extensive* coherent category. Of course, an arbitrary coherent category may not have all coproducts, and if it has coproducts they may not be disjoint (e.g. the posetal case). >> A second side-remark is this, which I realized just now while writing >> this, although I have known the above for several years: >> >> We know that the addition of propositional truncations as a rule, with >> certain stipulated definitional equalities, as in the HoTT book, gives >> function extensionality. >> >> A number of us (including Nicolai and me), asked whether hypothetical >> propositional truncations (which cannot come with stipulated >> definitional equalities) also give funext. >> >> The above argument shows that hypothetical propositional truncations >> definitely cannot give function extensionality. For, if this were the >> case, excluded middle would also imply function extensionality. But we >> know that this is not the case. >> >> Best, >> Martin