From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.99.116.4 with SMTP id p4mr4747294pgc.14.1494909259838; Mon, 15 May 2017 21:34:19 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.36.28.132 with SMTP id c126ls248631itc.5.gmail; Mon, 15 May 2017 21:34:19 -0700 (PDT) X-Received: by 10.99.157.137 with SMTP id i131mr4552404pgd.78.1494909259113; Mon, 15 May 2017 21:34:19 -0700 (PDT) Received: by 10.55.183.197 with SMTP id h188msqkf; Fri, 12 May 2017 11:10:04 -0700 (PDT) X-Received: by 10.28.158.83 with SMTP id h80mr379690wme.21.1494612604445; Fri, 12 May 2017 11:10:04 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1494612604; cv=none; d=google.com; s=arc-20160816; b=yq7oLwg9V+R+J7WHuggHsON/G8tdBlk5IlL/x6go3Un0/jL3Wj56dWG5hngfcl8SQi lZ8e5eQ/oaDLdFA7ODzzpMmYJuWY9s/ppylk6iZC2+n9VIbAjIhun4EJjpdmkmgHQPD1 ukZaXCFNjHI01vuMB1BmTwqpZ0kD8jhtxiuTeeLygbFZ6x/d/Tb3R8IWs0u9OnScL9Vt oIeD1tHUNfO/xPiThApuzZPaSUF/gkHid5tZOj7t88iTchjEIjX/PNHbS/JFeh2CCeGU Vi5kBgn7NtTfl+WVA9JG/lXJUn7LcQ6VSALq/lFAtFQTnFwUxfSPr0tn+1LcxrBLEa4v Jlvg== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:in-reply-to:mime-version:user-agent:date :message-id:cc:from:references:to:subject:arc-authentication-results; bh=vvPF+EkPIc3/luZczt2FJicrPJ31yj7pb8qUyDHG3VQ=; b=ndWOxmNi3AN/ZED2eqTPQUM9GEmNBMtTeFdlJRr2Dx4mgd03gAvgoSu1fc5mdQ5qnE FR9eIygoWolpbkGFhj1vRsZ1V05ZSv1UCwstE6doEXzKAYMT1dQh8paMdLyvilu4wp5w A0K+A+Rdb5cm8BGFm2NoSUSdvRzz/P8tHZ5EwmP09PRVpDARK1MBZhgArl/mbJzdsk9e KnnGxD+daMrPqcZ8aFlFIWvvcPEJ4zOE4pkpIWjr1bB0qgWb1LL0u9StP1itXasJ1D0M zagBpbOd8O26h2cppJuCSqXxK9zjzaKJxyGknMS1KywiYTkrEfrJpgQmBNMQ0vb+jhBT BiEQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=softfail (google.com: domain of transitioning escardo...@googlemail.com does not designate 147.188.128.150 as permitted sender) smtp.mailfrom=escardo...@googlemail.com; dmarc=fail (p=QUARANTINE sp=QUARANTINE dis=QUARANTINE) header.from=googlemail.com Return-Path: Received: from sun61.bham.ac.uk (sun61.bham.ac.uk. [147.188.128.150]) by gmr-mx.google.com with ESMTPS id 130si410707wmq.0.2017.05.12.11.10.04 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Fri, 12 May 2017 11:10:04 -0700 (PDT) Received-SPF: softfail (google.com: domain of transitioning escardo...@googlemail.com does not designate 147.188.128.150 as permitted sender) client-ip=147.188.128.150; Authentication-Results: gmr-mx.google.com; spf=softfail (google.com: domain of transitioning escardo...@googlemail.com does not designate 147.188.128.150 as permitted sender) smtp.mailfrom=escardo...@googlemail.com; dmarc=fail (p=QUARANTINE sp=QUARANTINE dis=QUARANTINE) header.from=googlemail.com Received: from [147.188.128.54] (helo=mailer3) by sun61.bham.ac.uk with esmtp (Exim 4.84) (envelope-from ) id 1d9F0u-0001FL-Mn; Fri, 12 May 2017 19:10:04 +0100 Received: from [31.185.238.126] (helo=[192.168.1.74]) by bham.ac.uk (envelope-from ) with esmtpsa (TLSv1.2:DHE-RSA-AES128-SHA:128) (Exim 4.84) id 1d9F0t-0005n3-G5 using interface auth-smtp.bham.ac.uk; Fri, 12 May 2017 19:10:04 +0100 Subject: Re: [HoTT] Does MLTT have "or"? To: Michael Shulman References: From: Martin Escardo Cc: "HomotopyT...@googlegroups.com" Message-ID: <1cef3819-ed3f-c684-d070-f49576045a19@googlemail.com> Date: Fri, 12 May 2017 19:10:03 +0100 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.8.0 MIME-Version: 1.0 In-Reply-To: Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: 8bit X-BHAM-SendViaRouter: yes X-BHAM-AUTH-data: TLSv1.2:DHE-RSA-AES128-SHA:128 via 147.188.128.21:465 (escardom) On 02/05/17 20:04, Michael Shulman wrote: > Some thoughts: > > [...] > > - A model of MLTT with function extensionality but no universes is > given by any locally cartesian closed category (perhaps with > coproducts if we have binary sum types). It seems that surely not > every lccc with coproducts is a regular category -- though I don't > have an example ready to hand, let alone an example that also has > universes. If you assume excluded middle (every proposition is empty or pointed), and function extensionality, then, as you know, every type X does have a propositional truncation, namely ¬¬X:=(X->0)->0. The universal map is the evaluation map eta:X->¬¬X. If we have f:X->P for a proposition P, then we get ¬¬f:¬¬X->¬¬P by the functoriality of double-dualization. By excluded middle we have a map ¬¬P->P, which composed with ¬¬f gives a map f':¬¬X->P, which in turn establishes the universality of eta:X->¬¬X among maps of X into propositions (the uniqueness requirement relies on funext). Therefore, indeed, ¬¬X is the propositional truncation of X (or, more precisely, ¬¬X, together with eta:X->¬¬X and the extension procedure f |-> f' and its uniqueness give the propositional truncation of X). (Side-remark. Conversely, if you forget the assumption of excluded middle, but remember the assumption of function extensionality, then the assumption that eta:X->¬¬X is the universal map of X into a proposition, for every X, implies excluded middle. (Exercise.) So, in general, the propositional truncation of X, if it exists, is wildly different from ¬¬X.) 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?). 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