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