From mboxrd@z Thu Jan 1 00:00:00 1970 Date: Thu, 25 Jan 2018 02:14:20 -0800 (PST) From: =?UTF-8?Q?Mart=C3=ADn_H=C3=B6tzel_Escard=C3=B3?= To: Homotopy Type Theory Message-Id: <8e5014ee-eaa1-47f3-abe0-56d49e50728f@googlegroups.com> In-Reply-To: References: <17bbe329-b471-490c-b11d-31c50f1334f1@googlegroups.com> Subject: Re: [HoTT] Re: Coquand's list of open problems MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_1650_329725277.1516875260356" ------=_Part_1650_329725277.1516875260356 Content-Type: multipart/alternative; boundary="----=_Part_1651_294715588.1516875260357" ------=_Part_1651_294715588.1516875260357 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable Right, this kind of thing is indeed what I have in mind. Another example (with Cory Knapp) is a lifting monad induced by a=20 dominance. Fix a universe U. Then its type of propositions, Prop, lives in= =20 the next universe U'. A dominance is a subset of Prop subject to certain=20 conditions. Prop itself is a dominance, and let's consider this for=20 simplicity. Then a partial element of a type X is a proposition P (the=20 extent of definition of the partial element) together with a function P->X.= =20 The lifting of X is then=20 LX :=3D Sigma(P:U), isProp P * (P->X).=20 If X is in a universe V, then LX is in the universe U' \/ V (namely the=20 least universe after U' and V, where we are assuming a sequence of=20 universes). However, if we apply L once more to get L(L X), this is in the= =20 same universe as L X (we increase the universe levels only once), and we=20 get well typed functions eta : X->LX and mu : L(LX)->LX that satisfy the=20 monad laws.=20 If we assume propositional resizing, then all propositions live in the=20 first universe U0, and so does Prop, and then L becomes a monad in the=20 usual sense. But it is not clear what is gained by this (in this example)= =20 other than getting something one is more familiar with. =20 In other examples, resizing does make a difference (of course). Consider=20 for example the assertion that Prop is a complete lattice with respect to= =20 the "->" ordering . If we say that every family has a least upper bound,=20 then we don't need resizing to prove that (we use the propositional=20 truncation of the sum of the family to calculate the join). But to get =20 that every *subset* of Prop (that is, map s : Prop->Prop) has a least upper= =20 bound, we would need resizing, as the natural candidate Sigma(P:Prop), s(P)= =20 is a proposition in the next universe and hence is not in Prop unless we=20 have resizing. In this second example, the problem is solved by working=20 with families rather than subsets. Are there examples in which there is no= =20 (known) way out without resizing? Martin On Wednesday, 24 January 2018 22:40:59 UTC, Nicola Gambino wrote: > > Dear Martin,=20 > > On 24 Jan 2018, at 22:36, Mart=C3=ADn H=C3=B6tzel Escard=C3=B3 > wrote: > > So one vague question is how much one can do *without* propositional=20 > resizing and living with the fact that universe levels may go up and down= =20 > in constructions such as the above. (A vague answer is "a lot", from my o= wn=20 > experience of formalizing things.)=20 > > A more precise question is that if we have a monad "up to universe=20 > juggling" (such as the above), what kind of universal property "up to=20 > universe juggling" does it correspond to.=20 > > > You may have a look at relative monads (Altenkirch et al) and relative=20 > pseudomonads (Fiore, Gambino, Hyland, Winskel). We considered the preshea= f=20 > construction that takes a small category to a locally small one (and henc= e=20 > jumps up a universe) as a relative pseudomonad. Here, =E2=80=9Cpseudo=E2= =80=9D refers to=20 > coherence issues, which I am not sure arise in type theory. > > Best wishes, > Nicola > > Dr Nicola Gambino > School of Mathematics, University of Leeds > Web: http://www1.maths.leeds.ac.uk/~pmtng/=20 > > ------=_Part_1651_294715588.1516875260357 Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: quoted-printable
Right, this kind of thing is indeed what I have in mind.
Another example (with Cory Knapp) is a lifting monad indu= ced by a dominance. Fix a universe U. Then its type of propositions, Prop, = lives in the next universe U'. A dominance is a subset of Prop subject = to certain conditions. Prop itself is a dominance, and let's consider t= his for simplicity. Then a partial element of a type X is a proposition P (= the extent of definition of the partial element) together with a function P= ->X. The lifting of X is then=C2=A0

=C2=A0 =C2= =A0LX :=3D Sigma(P:U), isProp P * (P->X).=C2=A0

If X is in a universe V, then LX is in the universe U' \/ V (namely th= e least universe after U' and V, where we are assuming a sequence of un= iverses). However, if we apply L once more to get L(L X), this is in the sa= me universe as L X (we increase the universe levels only once), and we get = well typed functions eta : X->LX and mu : L(LX)->LX that satisfy the = monad laws.=C2=A0

If we assume propositional resiz= ing, then all propositions live in the first universe U0, and so does Prop,= and then L becomes a monad in the usual sense. But it is not clear what is= gained by this (in this example) other than getting something one is more = familiar with.=C2=A0=C2=A0

In other examples, resi= zing does make a difference (of course). Consider for example the assertion= that Prop is a complete lattice with respect to the "->" orde= ring . If we say that every family has a least upper bound, then we don'= ;t need resizing to prove that (we use the propositional truncation of the = sum of the family to calculate the join). But to get=C2=A0 that every *subs= et* of Prop (that is, map s : Prop->Prop) has a least upper bound, we wo= uld need resizing, as the natural candidate Sigma(P:Prop), s(P) is a propos= ition in the next universe and hence is not in Prop unless we have resizing= . In this second example, the problem is solved by working with families ra= ther than subsets. Are there examples in which there is no (known) way out = without resizing?

Martin


On Wedn= esday, 24 January 2018 22:40:59 UTC, Nicola Gambino wrote:
Dear Martin,=C2=A0

On 24 Jan 2018, at 22:36, Mart=C3=ADn H=C3=B6tzel Escard=C3=B3 <escar...= @gmail.com> wrote:

So one vague question is how much one can do *without* propositional resizi= ng and living with the fact that universe levels may go up and down in cons= tructions such as the above. (A vague answer is "a lot", from my = own experience of formalizing things.)=C2=A0

A more precise question is that if we have a monad "up to universe jug= gling" (such as the above), what kind of universal property "up t= o universe juggling" does it correspond to.=C2=A0

You may have a look at relative monads (Altenkirch et al) and relative= pseudomonads (Fiore, Gambino, Hyland, Winskel). We considered the presheaf= construction that takes a small category to a locally small one (and hence= jumps up a universe) as a relative pseudomonad. Here, =E2=80=9Cpseudo=E2=80=9D refers to coherence issues, wh= ich I am not sure arise in type theory.

Best wishes,
Nicola

Dr Nicola Gambino
School of Mathematics, University of=C2=A0Leeds
Web:=C2=A0http://www1.maths.leeds.ac.uk/~= pmtng/

------=_Part_1651_294715588.1516875260357-- ------=_Part_1650_329725277.1516875260356--