From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.36.33.86 with SMTP id e83mr3645586ita.2.1494712023212; Sat, 13 May 2017 14:47:03 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.157.80.17 with SMTP id a17ls10724847oth.5.gmail; Sat, 13 May 2017 14:47:02 -0700 (PDT) X-Received: by 10.157.82.8 with SMTP id e8mr5353747oth.80.1494712022700; Sat, 13 May 2017 14:47:02 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1494712022; cv=none; d=google.com; s=arc-20160816; b=O7NRkdIvQkKP9VD4GicUXQ/8BCnKftCdV4eSXh3wioFI3RdVXBNYbxNkGRg7jZSvws l/snV0telagULg1t2iGJzrLAEDbDm8aTt4W0rXfbjtmOeLcTdOAigQRkLMfxs2VpMYSw kqtgCam7BqzYSXqCapPOubeI67myKd6KI7OO6TxvxtCyOEyxGzlJ4+vbvDtWf5XYXUPN X8wtZoee0QqmZXCmJvOMgwqmpsymySfz6TriKMEnbAnNiJDkA1P7V4OxeDTESg34kktm FIX+DEh7rIKcolZkMKCA87Buuyc0OTlhJh0pwyxM8UwBRUS5VQTSzL59B4QuzUkUIa6c HDHg== 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=q2e9W/7wEFFLj+uj/kDTyz70U7CFRW7m9p2VaLDCrvg=; b=w/IQVB1avPUuiJs7QrjM80jSeHstDr+UE3Md4iFjJ4B5iLUm652Dzeq3NEWtwSu2+X IS/3wbJa1jq4wbRFym7rnjiu0eQlgwV7+G70izvdHDnQwyFaer2A6JC9ynjyumG0DS6X cGKPMfGeEeeLRHAqD37eR3HKVNiIvj0hU7gBPmNq8Hs2a9KL7gZkiGFqXgB3LV5cwQUh FKpp/TMIAgFNg2ZbELIXYoGmDGoO+rEiHRhvayLmUFiY20QaUh6Kk9i5jDAO8was3aju OU6tsiDCx4QGSpRUxIihjoSOktSnRH64lhxe98J21R1QeUHikiH1Kd/1DUJ+tckGFurM lCfg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com; spf=neutral (google.com: 2607:f8b0:4002:c05::232 is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Return-Path: Received: from mail-yw0-x232.google.com (mail-yw0-x232.google.com. [2607:f8b0:4002:c05::232]) by gmr-mx.google.com with ESMTPS id p205si700475ywg.4.2017.05.13.14.47.02 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sat, 13 May 2017 14:47:02 -0700 (PDT) Received-SPF: neutral (google.com: 2607:f8b0:4002:c05::232 is neither permitted nor denied by domain of shu...@sandiego.edu) client-ip=2607:f8b0:4002:c05::232; Authentication-Results: gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com; spf=neutral (google.com: 2607:f8b0:4002:c05::232 is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Received: by mail-yw0-x232.google.com with SMTP id l74so9513339ywe.2 for ; Sat, 13 May 2017 14:47:02 -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=q2e9W/7wEFFLj+uj/kDTyz70U7CFRW7m9p2VaLDCrvg=; b=X6HP6YLAg9nq53d7aLegkgfS02kQQ3nk6HQ4UeQ+DMa5YRDMds9nMrVOWa/NOp0pdK y85BsN6XCuqTI80aCt7b5lvatZrDWwgwQeypJLJsKi0o51tPnxXoaP56/8kYnqnkE1eK Shu8nQfpSqP7UaQ5sLNamIeHRx37U6o2OYqDLAUL4hgCybqE5Z3X7C9ew8Qs/HHwL1vQ 31gUfoITrRpJE2pRnZKSSpoWylS8V1TLoBm1MtEEx567AIYdwaIp8x5ViISc3EaR3gXV zm8LPkRGrU9Bbtk/pr8+3fZOI3OwzWbdTJAYXOUV8bLOs8qJomC7pDnPgjHLUN50o/TW dQpw== X-Gm-Message-State: AODbwcBf8F0l+O1RindT4EgrYB08ccLOYD9DLxeT+PvnBMVfUPc/uZow 3EEM64zJqXx/ZrBAb4s= X-Received: by 10.129.161.85 with SMTP id y82mr9101711ywg.166.1494712022260; Sat, 13 May 2017 14:47:02 -0700 (PDT) Return-Path: Received: from mail-yw0-f171.google.com (mail-yw0-f171.google.com. [209.85.161.171]) by smtp.gmail.com with ESMTPSA id u187sm3363681ywg.65.2017.05.13.14.47.01 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sat, 13 May 2017 14:47:01 -0700 (PDT) Received: by mail-yw0-f171.google.com with SMTP id l74so9513286ywe.2 for ; Sat, 13 May 2017 14:47:01 -0700 (PDT) X-Received: by 10.129.145.69 with SMTP id i66mr8241832ywg.229.1494712021509; Sat, 13 May 2017 14:47:01 -0700 (PDT) MIME-Version: 1.0 Received: by 10.37.207.1 with HTTP; Sat, 13 May 2017 14:46:41 -0700 (PDT) In-Reply-To: <1cef3819-ed3f-c684-d070-f49576045a19@googlemail.com> References: <1cef3819-ed3f-c684-d070-f49576045a19@googlemail.com> From: Michael Shulman Date: Sat, 13 May 2017 14:46:41 -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 Fri, May 12, 2017 at 11:10 AM, Martin Escardo wrote: > The above argument relies on having a universe (first, to formulate > excluded middle and funext, and, second, to formulate and prove the > universality of eta). > > *** What is the interaction (if any) of excluded middle with regularity, > in your thought above? It seems to me that adding a universe is playing > a role. It is different to say externally that all morphisms have > images, than to say this internally using a universe (or am I wrong?). Three replies: 1. I don't think the argument technically relies on having a universe. LEM, funext, and the universality of eta are usually stated internally by quantifying over a universe, but they can also be stated as rules with type judgments as premises, and I believe the proof of universality goes through as a derivation of one rule from others. 2. In general, saying something internally is different from saying it externally, but I think that for images (and more generally for universal properties that are stable under pullback and descent) there is no difference. In such cases saying it internally with a universe is the same as saying it externally for the "universal case", which implies its external truth in all other cases. (You can also say it "internally" without a universe using stack semantics.) 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. > 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