Re: Coquand's list of open problems

["Martín Hötzel Escardó" <"escardo..."@gmail.com>]

[-- Attachment #1.1: Type: text/plain, Size: 2546 bytes --]

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 
>

[-- Attachment #1.2: Type: text/html, Size: 3623 bytes --]