From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.98.101.197 with SMTP id z188mr5191643pfb.13.1493958693602; Thu, 04 May 2017 21:31:33 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.107.178.204 with SMTP id b195ls1626254iof.0.gmail; Thu, 04 May 2017 21:31:32 -0700 (PDT) X-Received: by 10.107.46.132 with SMTP id u4mr20394456iou.97.1493958692952; Thu, 04 May 2017 21:31:32 -0700 (PDT) Received: by 10.55.169.204 with SMTP id s195msqke; Tue, 2 May 2017 23:47:55 -0700 (PDT) X-Received: by 10.46.82.153 with SMTP id n25mr3645895lje.1.1493794074627; Tue, 02 May 2017 23:47:54 -0700 (PDT) Return-Path: Received: from sun60.bham.ac.uk (sun60.bham.ac.uk. [147.188.128.137]) by gmr-mx.google.com with ESMTPS id n4si341290wmf.2.2017.05.02.23.47.54 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Tue, 02 May 2017 23:47:54 -0700 (PDT) Received-SPF: softfail (google.com: domain of transitioning escardo...@googlemail.com does not designate 147.188.128.137 as permitted sender) client-ip=147.188.128.137; Authentication-Results: gmr-mx.google.com; spf=softfail (google.com: domain of transitioning escardo...@googlemail.com does not designate 147.188.128.137 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 sun60.bham.ac.uk with esmtp (Exim 4.84) (envelope-from ) id 1d5o4n-0008KL-P2; Wed, 03 May 2017 07:47:53 +0100 Received: from [31.185.238.126] (helo=[192.168.1.93]) by bham.ac.uk (envelope-from ) with esmtpsa (TLSv1.2:DHE-RSA-AES128-SHA:128) (Exim 4.84) id 1d5o4n-0004N7-F5 using interface auth-smtp.bham.ac.uk; Wed, 03 May 2017 07:47:53 +0100 Subject: Re: [HoTT] Does MLTT have "or"? To: Michael Shulman , Martin Escardo References: From: Martin Escardo Cc: "HomotopyT...@googlegroups.com" Message-ID: <86ba230d-8ec8-9ffe-8cb1-80c30fa25853@googlemail.com> Date: Wed, 3 May 2017 07:47:53 +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; format=flowed 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: Thanks. Some more remarks: > - If in addition to function extensionality and propositional > extensionality we assume propositional resizing, then ||-|| is > constructible using the standard argument that an elementary topos is > a regular category. We can say more regarding resizing, in the presence of universes, as in my question. If U' is the universe after U with U:U', then the large type hasTruncation'(X:U) := Σ(X':U'), isProp(X') × (X→X') × Π(P:U), (isProp(P) × (X→P)) → (X'→P). is always inhabited in MLTT. It is a proposition for all X:U iff funext and propext hold. Moreover, you can construct such a "large truncation" X' by X' = Π(P:U), isProp(P) → (X → P) → P. Then X' is a proposition for all X' iff funext holds (propext is not involved here). Then, in the presence of funext, X has a small truncation ∥X∥ iff there is a small proposition P:U equivalent to X', and in this case P has the universal property of ∥X∥. Hence the presence of all small propositional truncations *is* a resizing axiom, amounting to say that every large truncation X' of each small X:U is equivalent to some small P:U. > - 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. Right. I want an example with universes, and, moreover, an example which will not only fail to have all small truncations but also the truncation of P+Q for small propositions P and Q. You can ask this question when P and Q are type variables or when they are closed type terms. In many cases, a small truncation ∥P+Q∥ exists in all models, by a construction in MLTT. For example, consider α,β:ℕ→2 with isProp(Σ(n:ℕ), α(n)=1), isProp(Σ(n:ℕ), β(n)=1), and take P := Σ(n:ℕ), α(n)=1, Q := Σ(n:ℕ), β(n)=1. Then we can easily construct γ:ℕ→2 from α and β so that the type Σ(n:ℕ), γ(n)=1 has the universal property of ∥P+Q∥. Can you find examples of propositions P and Q such that their disjunction ∥P+Q∥ cannot be shown to exist in intensional MLTT with universes? Of course, we may have Π(P,Q:U), isProp(P) → isProp(Q) → hasTruncation(P×Q) empty in a model without such a counter-example P and Q. Martin > > > On Tue, May 2, 2017 at 2:09 AM, 'Martin Escardo' via Homotopy Type > Theory wrote: >> Last week in a meeting I had a technical discussion with somebody, who >> suggested to post the question here. >> >> (1) Prove (internally) or disprove (as a meta-theorem, probably with a >> counter-model) the following in (intensional) Martin-Loef Type Theory: >> >> * The poset of subsingletons (or propositions or truth values) has >> binary joins (or disjunction). >> >> (We know it has binary meets and Heyting implication, which amounts to >> saying it is a Heyting semilattice. Is it a lattice?) >> >> (2) The question is whether given any two propositions P and Q we can >> find a proposition R with P->R and Q->R such that for any proposition >> R' with P->R' and Q->R' we have R->R'. (R is the least upper bound of >> P and Q.) >> >> (3) Of course, if MLTT had propositional truncations ||-||, then the >> answer would be R := ||P+Q||. But we can ask this question for MLTT >> before we postulate propositional truncations as in (1)-(2). >> >> (4) What is a model of intensional MLTT with a universe such that >> ||-|| doesn't exist? >> >> More precisely, define, internally in intensional MLTT, >> >> hasTruncation(X:U) := Σ(X':U), >> isProp(X') >> × (X→X') >> × Π(P:U), (isProp(P) × (X→P)) → (X'→P). >> >> Is there a model, with universes, the falsifies this? >> >> Preferably, we want models that falsify this but validate >> function extensionality (and perhaps also propositional >> extensionality). >> >> Best, >> Martin >> >> -- >> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. >> To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeThe...@googlegroups.com. >> For more options, visit https://groups.google.com/d/optout. > -- Martin Escardo http://www.cs.bham.ac.uk/~mhe