Re: [HoTT] Re: Coquand's list of open problems

[Nicola Gambino <N.Ga...@leeds.ac.uk>]

[-- Attachment #1: Type: text/plain, Size: 1062 bytes --]

Dear Martin,

On 24 Jan 2018, at 22:36, Martín Hötzel Escardó <escardo...@gmail.com<mailto:escardo...@gmail.com>> wrote:

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.

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, “pseudo” refers to 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/


[-- Attachment #2: Type: text/html, Size: 2670 bytes --]