From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.107.132.37 with SMTP id g37mr4505191iod.81.1494909259822; Mon, 15 May 2017 21:34:19 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.36.108.210 with SMTP id w201ls1472729itb.5.canary-gmail; Mon, 15 May 2017 21:34:19 -0700 (PDT) X-Received: by 10.99.114.29 with SMTP id n29mr4603343pgc.90.1494909259117; Mon, 15 May 2017 21:34:19 -0700 (PDT) Received: by 10.55.183.197 with SMTP id h188msqkf; Fri, 12 May 2017 11:41:21 -0700 (PDT) X-Received: by 10.28.125.200 with SMTP id y191mr336689wmc.6.1494614481052; Fri, 12 May 2017 11:41:21 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1494614481; cv=none; d=google.com; s=arc-20160816; b=Of71TQyF6Olc3zlIE4tDJ722fMlvbzpmJUaQ6enEQAYwDSVs7bIIH2a0BzzkJmUM0F nQ7qEOR/j6YTgOfEqLk8blDGb00LB+yyvpowVhbWd4xDG7Izik86gD/pJ+Km7XgyqX5N 0K0tbFIwYwvPZ+CYiMOfI8BOTxw2Q+NgsfR5M6XZqMGEqu16gjiIYz0CWAiWbDhqvwwS noMJnu2UH/fRhOHBCq6pX1beLOQSC4ziwgV5xI0l/I2mq8nleCrN6VA9aUKyKMrzzebB fU40etSMGVolvAbKTChzhvYL9KkctI2O9Rpj8kB6paz/b5saEPyAe053Sn1pzbvnCb79 Tmzw== 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:from:cc:references:to:subject:arc-authentication-results; bh=d36INQVF6xzYIt+odeuDLaNongWRISLQxK/c39B2NzA=; b=iRxDAwHEi9/0EszlbPoI3miixzrLuf2g/L6ln/eIgt1jSHMIF+zJIpLdaXGwBXQveu 22KRqyqhhF7gc241rKJpJchMrBF76bi7jjRgG11L1xn8jTG3Y8mr2PmW4urZXrTWz7iR 5KQ0Ahe+rdxPs1femHbxJ8XXUYhJkXi8gqZ1ZgcjsQOo0tm8itydCdm6MmQ38pLcDooK EndfWrhuJBiS3QK6VPjMKXz7Owz+eD7QxuStEucyzmzOWMJ9zJ8jNSjgfC37K15ZmRsq GmDYq7nLSswKm/U3aTmWmN5IFjpidshgj7aMBTzkljVR0rSm2YaKqsthHjXATRkebzCU dscQ== 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 g11si173354wme.2.2017.05.12.11.41.21 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Fri, 12 May 2017 11:41:21 -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 1d9FVA-0003T1-PB; Fri, 12 May 2017 19:41:20 +0100 Received: from [31.185.238.126] (helo=[192.168.1.75]) by bham.ac.uk (envelope-from ) with esmtpsa (TLSv1.2:DHE-RSA-AES128-SHA:128) (Exim 4.84) id 1d9FVA-0001ZU-FF using interface auth-smtp.bham.ac.uk; Fri, 12 May 2017 19:41:20 +0100 Subject: Re: [HoTT] Does MLTT have "or"? To: Michael Shulman References: <1cef3819-ed3f-c684-d070-f49576045a19@googlemail.com> Cc: "HomotopyT...@googlegroups.com" From: Martin Escardo Message-ID: <63d3efb4-134b-8851-b41c-6b9a5533d176@googlemail.com> Date: Fri, 12 May 2017 19:41:20 +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: <1cef3819-ed3f-c684-d070-f49576045a19@googlemail.com> 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) Obviously the second side-remark overlooks the fact that we used function extensionality to show that excluded middle implies the existence of propositional truncations. Apologies. Hence the question of whether hypothetical propositional truncations imply function extensionality remains open (although I very much doubt that they do). Martin On 12/05/17 19:10, Martin Escardo wrote: > 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 >