From mboxrd@z Thu Jan 1 00:00:00 1970 Date: Wed, 24 Jan 2018 14:36:14 -0800 (PST) From: =?UTF-8?Q?Mart=C3=ADn_H=C3=B6tzel_Escard=C3=B3?= To: Homotopy Type Theory Message-Id: <17bbe329-b471-490c-b11d-31c50f1334f1@googlegroups.com> In-Reply-To: References: Subject: Re: Coquand's list of open problems MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_147_1920913412.1516833374490" ------=_Part_147_1920913412.1516833374490 Content-Type: multipart/alternative; boundary="----=_Part_148_979909594.1516833374491" ------=_Part_148_979909594.1516833374491 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 7bit Thanks for posting this. I am particularly interested in Problem 3, namely propositional resizing, although of course all problems are relevant and interesting. When one starts transcribing classical mathematics in constructive type theory, it is not only excluded middle and choice that arise as obstacles, but also the fact that a number of constructions don't preserve universe levels (such as powersets, ideal completions, spaces of filters, etc), as is well-known. So a positive solution to Problem 3 gets this out of the way. However, in the absence of resizing, life doesn't look that bad, at least at first sight. For example, the powerset construction (-) -> Prop (once we fix the type Prop for a particular universe) is not a monad because of the violation of universe levels, but other than that is has all the expected structure needed to define a monad, as well as the required properties. So one vague question is how much one can do *without* propositional resizing and living with the fact that universe levels may go up and down in constructions such as the above. (A vague answer is "a lot", from my own experience of formalizing things.) A more precise question is that if we have a monad "up to universe juggling" (such as the above), what kind of universal property "up to universe juggling" does it correspond to. This problem doesn't arise in 1-topos theory, which, by stipulation, has propositional resizing of sorts, as this is implied by the very definition of subobject classifier. But it seems that this is not a problem in a univalent type theory: Maps X->Prop (even if Prop may be in a universe higher than that of X) correspond to embeddings X'->X. Propositional resizing then probably arises by analogy from 1-topos theory. But is it really needed? This is not a rhetorical question, but a genuine "operational" mathematical question: how does life without resizing look like? We know a lot about how life without excluded middle (and hence choice) looks like, but I think we know much less about life without propositional resizing. I propose this as " Problem 3' ". Martin On Wednesday, 24 January 2018 15:14:05 UTC, Bas Spitters wrote: > > At the EUTypes meeting Thierry presented a list of five open problems in > HoTT. > I've added them here. Maybe they should be moved to the various > categories we have there. > However, I did not immediately see where to put them. > > > https://ncatlab.org/homotopytypetheory/show/open+problems#coquands_five_open_problems > ------=_Part_148_979909594.1516833374491 Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: quoted-printable
Thanks for posting this.

I am particula= rly interested in Problem 3, namely propositional resizing, although of cou= rse all problems are relevant and interesting.

Whe= n one starts transcribing classical mathematics in constructive type theory= , it is not only excluded middle and choice that arise as obstacles, but al= so the fact that a number of constructions don't preserve universe leve= ls (such as powersets, ideal completions, spaces of filters, etc), as is we= ll-known. So a positive solution to Problem 3 gets this out of the way.

However, in the absence of resizing, life doesn't= look that bad, at least at first sight. For example, the powerset construc= tion (-) -> Prop (once we fix the type Prop for a particular universe) i= s not a monad because of the violation of universe levels, but other than t= hat is has all the expected structure needed to define a monad, as well as = the required properties.=C2=A0

So one vague qu= estion is how much one can do *without* propositional resizing and living w= ith the fact that universe levels may go up and down in constructions such = as the above. (A vague answer is "a lot", from my own experience = of formalizing things.)=C2=A0

A more precise quest= ion is that if we have a monad "up to universe juggling" (such as= the above), what kind of universal property "up to universe juggling&= quot; does it correspond to.=C2=A0

This problem do= esn't arise in 1-topos theory, which, by stipulation, has propositional= resizing of sorts, as this is implied by the very definition of subobject = classifier. But it seems that this is not a problem in a univalent type the= ory: Maps X->Prop (even if Prop may be in a universe higher than that of= X) correspond to embeddings X'->X. Propositional resizing then prob= ably arises by analogy from 1-topos theory. But is it really needed? This i= s not a rhetorical question, but a genuine "operational" mathemat= ical question: how does life without resizing look like? We know a lot abou= t how life without excluded middle (and hence choice) looks like, but I thi= nk we know much less about life without propositional resizing. I propose t= his as "=C2=A0 Problem 3'=C2=A0 ".

M= artin




On Wednesday, 24 Janu= ary 2018 15:14:05 UTC, Bas Spitters wrote:
At the EUTypes meeting Thierry presented a list of five open p= roblems in HoTT.
I've added them here. Maybe they should be moved to the various
categories we have there.
However, I did not immediately see where to put them.

https://ncatlab.org/homotop= ytypetheory/show/open+problems#coquands_five_open_problems
------=_Part_148_979909594.1516833374491-- ------=_Part_147_1920913412.1516833374490--