From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.157.23.167 with SMTP id j36mr1062897otj.115.1494363048778; Tue, 09 May 2017 13:50:48 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.157.39.14 with SMTP id r14ls1154158ota.15.gmail; Tue, 09 May 2017 13:50:48 -0700 (PDT) X-Received: by 10.13.202.17 with SMTP id m17mr1076857ywd.120.1494363048330; Tue, 09 May 2017 13:50:48 -0700 (PDT) Received: by 10.55.108.69 with SMTP id h66msqkc; Sun, 7 May 2017 06:49:52 -0700 (PDT) X-Received: by 10.46.21.66 with SMTP id 2mr578683ljv.8.1494164992332; Sun, 07 May 2017 06:49:52 -0700 (PDT) Return-Path: Received: from sun61.bham.ac.uk (sun61.bham.ac.uk. [147.188.128.150]) by gmr-mx.google.com with ESMTPS id f136si711809wme.1.2017.05.07.06.49.52 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sun, 07 May 2017 06:49:52 -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 1d7MZM-0006Ic-Ms for HomotopyT...@googlegroups.com; Sun, 07 May 2017 14:49:52 +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 1d7MZM-0005gp-Cu for HomotopyT...@googlegroups.com using interface auth-smtp.bham.ac.uk; Sun, 07 May 2017 14:49:52 +0100 Subject: Re: [HoTT] Re: Does MLTT have "or"? To: Homotopy Type Theory References: From: Martin Escardo Message-ID: <77e5eee5-a160-dcc9-bd7d-5e6061cbd9e4@googlemail.com> Date: Sun, 7 May 2017 14:49:51 +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) Interesting! Martin On 06/05/17 14:51, Andrew Swan wrote: > We consider the category "localisation of setoids." That is we take the > objects to be sets equipped with an equivalence relation (X, ~), and > morphisms (X, ~) -> (Y, ~) to be functions f: X/~ -> Y/~ such that there > exists a function f': X -> Y commuting with f and the quotient maps. In > ZFC we can show that this category is equivalent to Set, so we already > know it is complete, cocomplete and locally cartesian closed. However, > it will be important that we can also do this constructively i.e. > without using the equivalence with Set. Note that one can give explicit > definitions of limits and colimits as well as dependent products that > work constructively. > > Say that a setoid is trivial if the equivalence classes are all > singletons. The full subcategory of trivial setoids is isomorphic to the > category of sets (and this time the isomorphism works constructively). > > Note that image factorisation is different in trivial setoids and > setoids. Suppose we have some morphism of trivial setoids f: (X, ~) -> > (Y, ~) (since these are trivial setoids this is just any map X -> Y). > For the image factorisation in setoids, we take the underlying set of > im(f) to be X, but change the equivalence relation, to ~' defined by x > ~' x' whenever f(x) = f(x'). On the other hand the image factorisation > in trivial setoids is the quotient X/~' together with the trivial > equivalence relation. Assuming choice these will be isomorphic. However, > the key point is that in general the converse also holds, so by working > internally in a model of set theory where AC fails, we can get examples > where the image factorisations are not isomorphic (ie where the > inclusion of subcategory functor does not preserve image factorisation). > > On the other hand, the rest of the type theoretic structure is preserved > by the inclusion functor. Dependent products, finite limits and disjoint > sums are all the same in trivial setoids and setoids. > > We now assume that we have an inaccessible set, stated using a suitable > constructive notion of inaccessible. We define a universe U_1 -> U_0 by > taking U_0 to be the set of all small trivial setoids, and an element of > U_1 is a small trivial setoid together with one of its elements. Take > the equivalence relation on U_1 and U_2 to just be trivial. The small > maps f: X -> Y are then those which are both small in the usual sense > (fibres are isomorphic to elements of the inaccessible set), and also > admit a function f': X -> Y which makes a pullback square with f and the > quotient maps. Note that if Y is trivial and f: X -> Y is small then X > is also trivial. We can also consider another larger universe V_1 -> V_0 > which consists of all small setoids. > > If we interpret type theory in the above category we can almost, but not > quite answer question (4). We work internally in the Lifschitz > realizability model like in Chen, Rathjen, Lifschitz realizability for > intuitionistic Zermelo–Fraenkel set theory > . In type > theory we work over the context consisting of binary sequences a: N -> 2 > which are 1 at most once, and we consider the propositions P(a) = forall > n. a(2n) = 0 and Q(a) = forall n. a(2n + 1) = 0. Call this context A. > Then LLPO is the statement that for all a in A, the proposition P(a) \/ > Q(a) is true (when disjunction exists at all). If the disjunction ||P \/ > Q|| exists, then we would have maps of the form P + Q -> || P + Q || -> > A in the model. If || P + Q || belongs to the universe U, then the map > || P + Q || -> A would be small, which would make the setoid || P + Q || > trivial, and in particular it has to be just a subset of A. On the other > hand, if this is still the disjunction of P and Q when we move up to the > larger universe V, then it has to be isomorphic to the "real" image > factorisation in setoids, which consists of pairs (i, a) where either i > = 0 and P(a) holds or i = 1 and Q(a) holds, together with the > equivalence relation that identifies (0, a) and (1, a) when both occur > in the set. If this was isomorphic to a monomorphism, then, assuming > LLPO, we would have a choice function, that selects for each a in A, a > choice of i such that i = 0 and P(a) or i = 1 and Q(a). However this is > impossible in Lifschitz realizability. > > I think it's possible to get a complete answer to question (4) by > instead working with the arrow category of setoids, and then > interpreting the universe as the inclusion of U into V. > > Finally, the above was working over a context, A, but I think it's also > possible to do the same over the empty context, because I have some > unpublished results that imply there is a specific computable sequence > a: N -> 2 such that IZF + LLPO + MP proves a has at most one 1, but for > any definable set, x, IZF + LLPO + MP cannot prove the statement "x > belongs to 2, and either x = 0 and P(a) holds or x = 1 and Q(a) holds". > > > Best, > Andrew > > > On Tuesday, 2 May 2017 18:45:41 UTC+2, Martín Hötzel Escardó 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.