From mboxrd@z Thu Jan 1 00:00:00 1970 Date: Sat, 6 May 2017 06:51:02 -0700 (PDT) From: Andrew Swan To: Homotopy Type Theory Message-Id: In-Reply-To: References: Subject: Re: Does MLTT have "or"? MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_1432_1785469378.1494078662480" ------=_Part_1432_1785469378.1494078662480 Content-Type: multipart/alternative; boundary="----=_Part_1433_726360012.1494078662481" ------=_Part_1433_726360012.1494078662481 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable We consider the category "localisation of setoids." That is we take the=20 objects to be sets equipped with an equivalence relation (X, ~), and=20 morphisms (X, ~) -> (Y, ~) to be functions f: X/~ -> Y/~ such that there=20 exists a function f': X -> Y commuting with f and the quotient maps. In ZFC= =20 we can show that this category is equivalent to Set, so we already know it= =20 is complete, cocomplete and locally cartesian closed. However, it will be= =20 important that we can also do this constructively i.e. without using the=20 equivalence with Set. Note that one can give explicit definitions of limits= =20 and colimits as well as dependent products that work constructively. Say that a setoid is trivial if the equivalence classes are all singletons.= =20 The full subcategory of trivial setoids is isomorphic to the category of=20 sets (and this time the isomorphism works constructively). Note that image factorisation is different in trivial setoids and setoids.= =20 Suppose we have some morphism of trivial setoids f: (X, ~) -> (Y, ~) (since= =20 these are trivial setoids this is just any map X -> Y). For the image=20 factorisation in setoids, we take the underlying set of im(f) to be X, but= =20 change the equivalence relation, to ~' defined by x ~' x' whenever f(x) =3D= =20 f(x'). On the other hand the image factorisation in trivial setoids is the= =20 quotient X/~' together with the trivial equivalence relation. Assuming=20 choice these will be isomorphic. However, the key point is that in general= =20 the converse also holds, so by working internally in a model of set theory= =20 where AC fails, we can get examples where the image factorisations are not= =20 isomorphic (ie where the inclusion of subcategory functor does not preserve= =20 image factorisation). On the other hand, the rest of the type theoretic structure is preserved by= =20 the inclusion functor. Dependent products, finite limits and disjoint sums= =20 are all the same in trivial setoids and setoids. We now assume that we have an inaccessible set, stated using a suitable=20 constructive notion of inaccessible. We define a universe U_1 -> U_0 by=20 taking U_0 to be the set of all small trivial setoids, and an element of=20 U_1 is a small trivial setoid together with one of its elements. Take the= =20 equivalence relation on U_1 and U_2 to just be trivial. The small maps f: X= =20 -> Y are then those which are both small in the usual sense (fibres are=20 isomorphic to elements of the inaccessible set), and also admit a function= =20 f': X -> Y which makes a pullback square with f and the quotient maps. Note= =20 that if Y is trivial and f: X -> Y is small then X is also trivial. We can= =20 also consider another larger universe V_1 -> V_0 which consists of all=20 small setoids. If we interpret type theory in the above category we can almost, but not=20 quite answer question (4). We work internally in the Lifschitz=20 realizability model like in Chen, Rathjen, Lifschitz realizability for=20 intuitionistic Zermelo=E2=80=93Fraenkel set theory=20 . In type=20 theory we work over the context consisting of binary sequences a: N -> 2=20 which are 1 at most once, and we consider the propositions P(a) =3D forall = n.=20 a(2n) =3D 0 and Q(a) =3D forall n. a(2n + 1) =3D 0. Call this context A. Th= en=20 LLPO is the statement that for all a in A, the proposition P(a) \/ Q(a) is= =20 true (when disjunction exists at all). If the disjunction ||P \/ Q||=20 exists, then we would have maps of the form P + Q -> || P + Q || -> A in=20 the model. If || P + Q || belongs to the universe U, then the map || P + Q= =20 || -> A would be small, which would make the setoid || P + Q || trivial,=20 and in particular it has to be just a subset of A. On the other hand, if=20 this is still the disjunction of P and Q when we move up to the larger=20 universe V, then it has to be isomorphic to the "real" image factorisation= =20 in setoids, which consists of pairs (i, a) where either i =3D 0 and P(a)=20 holds or i =3D 1 and Q(a) holds, together with the equivalence relation tha= t=20 identifies (0, a) and (1, a) when both occur in the set. If this was=20 isomorphic to a monomorphism, then, assuming LLPO, we would have a choice= =20 function, that selects for each a in A, a choice of i such that i =3D 0 and= =20 P(a) or i =3D 1 and Q(a). However this is impossible in Lifschitz=20 realizability. I think it's possible to get a complete answer to question (4) by instead= =20 working with the arrow category of setoids, and then interpreting the=20 universe as the inclusion of U into V. Finally, the above was working over a context, A, but I think it's also=20 possible to do the same over the empty context, because I have some=20 unpublished results that imply there is a specific computable sequence a: N= =20 -> 2 such that IZF + LLPO + MP proves a has at most one 1, but for any=20 definable set, x, IZF + LLPO + MP cannot prove the statement "x belongs to= =20 2, and either x =3D 0 and P(a) holds or x =3D 1 and Q(a) holds". Best, Andrew On Tuesday, 2 May 2017 18:45:41 UTC+2, Mart=C3=ADn H=C3=B6tzel Escard=C3=B3= wrote: > > Last week in a meeting I had a technical discussion with somebody, who=20 > suggested to post the question here.=20 > > (1) Prove (internally) or disprove (as a meta-theorem, probably with a=20 > counter-model) the following in (intensional) Martin-Loef Type Theory:=20 > > * The poset of subsingletons (or propositions or truth values) has=20 > binary joins (or disjunction).=20 > > (We know it has binary meets and Heyting implication, which amounts to=20 > saying it is a Heyting semilattice. Is it a lattice?)=20 > > (2) The question is whether given any two propositions P and Q we can=20 > find a proposition R with P->R and Q->R such that for any proposition=20 > R' with P->R' and Q->R' we have R->R'. (R is the least upper bound of=20 > P and Q.)=20 > > (3) Of course, if MLTT had propositional truncations ||-||, then the=20 > answer would be R :=3D ||P+Q||. But we can ask this question for MLTT=20 > before we postulate propositional truncations as in (1)-(2).=20 > > (4) What is a model of intensional MLTT with a universe such that=20 > ||-|| doesn't exist?=20 > > More precisely, define, internally in intensional MLTT,=20 > > hasTruncation(X:U) :=3D =CE=A3(X':U),=20 > isProp(X')=20 > =C3=97 (X=E2=86=92X')=20 > =C3=97 =CE=A0(P:U), (isProp(P) =C3=97 (X=E2=86= =92P)) =E2=86=92 (X'=E2=86=92P).=20 > > Is there a model, with universes, the falsifies this?=20 > > Preferably, we want models that falsify this but validate=20 > function extensionality (and perhaps also propositional=20 > extensionality).=20 > > Best,=20 > Martin=20 > ------=_Part_1433_726360012.1494078662481 Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: quoted-printable
We consider the category "localisation of setoids.&qu= ot; That is we take the objects to be sets equipped with an equivalence rel= ation (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 constructiv= ely i.e. without using the equivalence with Set. Note that one can give exp= licit definitions of limits and colimits as well as dependent products that= work constructively.

Say that a setoid is trivial if th= e equivalence classes are all singletons. The full subcategory of trivial s= etoids is isomorphic to the category of sets (and this time the isomorphism= works constructively).

Note that image factorisat= ion is different in trivial setoids and setoids. Suppose we have some morph= ism of trivial setoids f: (X, ~) -> (Y, ~) (since these are trivial seto= ids 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 r= elation, to ~' defined by x ~' x' whenever f(x) =3D f(x'). = On the other hand the image factorisation in trivial setoids is the quotien= t X/~' together with the trivial equivalence relation. Assuming choice = these will be isomorphic. However, the key point is that in general the con= verse also holds, so by working internally in a model of set theory where A= C fails, we can get examples where the image factorisations are not isomorp= hic (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 setoi= ds and setoids.

We now assume that we have an inac= cessible 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 j= ust be trivial. The small maps f: X -> Y are then those which are both s= mall in the usual sense (fibres are isomorphic to elements of the inaccessi= ble set), and also admit a function f': X -> Y which makes a pullbac= k 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 rea= lizability model like in Chen, Rathjen,=C2=A0Lifschitz realizability for intui= tionistic Zermelo=E2=80=93Fraenkel set theory. In type theory we work o= ver the context consisting of binary sequences a: N -> 2 which are 1 at = most once, and we consider the propositions P(a) =3D forall n. a(2n) =3D 0 = and Q(a) =3D forall n. a(2n + 1) =3D 0. Call this context A. Then LLPO is t= he statement that for all a in A, the proposition P(a) \/ Q(a) is true (whe= n 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 par= ticular it has to be just a subset of A. On the other hand, if this is stil= l 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 set= oids, which consists of pairs (i, a) where either i =3D 0 and P(a) holds or= i =3D 1 and Q(a) holds, together with the equivalence relation that identi= fies (0, a) and (1, a) when both occur in the set. If this was isomorphic t= o a monomorphism, then, assuming LLPO, we would have a choice function, tha= t selects for each a in A, a choice of i such that i =3D 0 and P(a) or i = =3D 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 the= n interpreting the universe as the inclusion of U into V.

Finally, the above was working over a context, A, but I t= hink 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 s= equence 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 &q= uot;x belongs to 2, and either x =3D 0 and P(a) holds or x =3D 1 and Q(a) h= olds".


Best,
Andrew<= /div>


On Tuesday, 2 May 2017 18:45:41 UTC+2, Mart=C3=ADn H=C3= =B6tzel Escard=C3=B3 wrote:
La= st 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:

=C2=A0 =C2=A0 * The poset of subsingletons (or propositions or truth va= lues) has
=C2=A0 =C2=A0 =C2=A0 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 proposi= tion
R' with P->R' and Q->R' we have R->R'. (R is t= he least upper bound of
P and Q.)

(3) Of course, if MLTT had propositional truncations ||-||, then the
answer would be R :=3D ||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,

=C2=A0 hasTruncation(X:U) :=3D =CE=A3(X':U),
=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 = =C2=A0 =C2=A0 =C2=A0 =C2=A0 isProp(X')
=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 = =C2=A0 =C2=A0 =C2=A0 =C3=97 (X=E2=86=92X')
=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 = =C2=A0 =C2=A0 =C2=A0 =C3=97 =CE=A0(P:U), (isProp(P) =C3=97 (X=E2=86=92P)) = =E2=86=92 (X'=E2=86=92P).

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
------=_Part_1433_726360012.1494078662481-- ------=_Part_1432_1785469378.1494078662480--