From mboxrd@z Thu Jan 1 00:00:00 1970 Date: Wed, 3 May 2017 05:17:31 -0700 (PDT) From: Andrew Polonsky To: Homotopy Type Theory Message-Id: <0972e3bc-7d2c-46ae-a644-a94ede4e8724@googlegroups.com> In-Reply-To: References: Subject: Re: Does MLTT have "or"? MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_1018_37746882.1493813851303" ------=_Part_1018_37746882.1493813851303 Content-Type: multipart/alternative; boundary="----=_Part_1019_1894406641.1493813851303" ------=_Part_1019_1894406641.1493813851303 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable If you don't mind the proposition living in a higher universe, then=20 certainly the impredicative encoding will do: P\/Q :=3D =E2=88=8F(X:U) isProp(X) -> (P -> X) -> (Q -> X) -> X satisfies P -> P\/Q Q -> P\/Q isProp(R) -> (P->R) -> (Q->R) -> (P\/Q -> R) Best, Andrew On Tuesday, May 2, 2017 at 12:45:41 PM UTC-4, Martin Hotzel Escardo 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_1019_1894406641.1493813851303 Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: quoted-printable
If you don't mind the proposition living in a higher u= niverse, then certainly the impredicative encoding will do:

<= div>P\/Q =C2=A0:=3D =C2=A0=E2=88=8F(X:U) isProp(X) -> (P -> X) -> = (Q -> X) -> X

satisfies

=
P -> P\/Q
Q -> P\/Q
isProp(R) -> (P->R= ) -> (Q->R) -> (P\/Q -> R)

Best,
=
Andrew

On Tuesday, May 2, 2017 at 12:45:41 PM UTC-4, Martin Hot= zel Escardo 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:

=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_1019_1894406641.1493813851303-- ------=_Part_1018_37746882.1493813851303--