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

[Bas Spitters <b.a.w.s...@gmail.com>]

> life without propositional resizing
That's what used to be called predicativity, isn't it :-)

More seriously, yes, in my experience, working in HoTT with a large
universe polymorphic hProp one can nicely encapsulate some of the
predicativity issues.
But we definitively need more experience doing it.

Are you aware of the relative universes presentation of CwFs?
Ahrens, Lumsdaine, Voevodsky:
https://arxiv.org/abs/1705.04310

On Wed, Jan 24, 2018 at 11:40 PM, Nicola Gambino <N.Ga...@leeds.ac.uk> wrote:
> Dear Martin,
>
> On 24 Jan 2018, at 22:36, Martín Hötzel Escardó <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/
>
> --
> You received this message because you are subscribed to the Google Groups
> "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to HomotopyTypeThe...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.