Re: [HoTT] Injective types

[Michael Shulman <shulman@sandiego.edu>]

Interesting point!  I definitely agree that we don't want to be
*forced* to be typically ambiguous; there are times when we need to
explicitly distinguish universes.  This was already the case in a few
places in the book, e.g. Lemmas 10.3.21 and 10.3.22.  And Coq's
universe polymorphism now also *allows* the user to explicitly specify
universe levels when desired.  (On the other hand, it's also nice to
not be forced to label all universes explicitly all the time.  But on
the third hard, at least in Coq as it is now, the interaction of
user-specified universes with automatically-deduced ones seems to be
fairly fragile.)

However, it's not clear to me why cumulativity would be a problem.  In
fact you wrote in the paper that "We don't assume that the universes
are cumulative... but we also don't assume that they are not".  Which
makes it sound as though cumulativity, though not necessary, wouldn't
be a problem if it did hold -- would it?

On Tue, Apr 30, 2019 at 4:05 PM <escardo.martin@gmail.com> wrote:
>
> I would like to advertise this paper, which investigates injective types and algebraically injective types, and their relationship (https://arxiv.org/abs/1903.01211).
>
> In this paper, it is important to take universe levels seriously (for the reasons explained there). In the HoTT book, and in Coq, the universes are taken to be cumulative on the nose, and we pretend, notationally, that there is only one universe (this is called typical ambiguity). Based on the experience of this paper, I have the feeling that the loss of cumulativity, as in Agda, but also as in the infty-topos model of univalent type theory by Mike (https://arxiv.org/abs/1904.07004) is a good thing. In particular, I am not sure how typical ambiguity with cumulativity would be able to handle what is said in the above injectives paper.
>
> When I say "would be able to handle" I don't mean just "accepting the constructions", but also present them to the (mathematical) user in such a way that is both understandable and usable as a blackbox (by quoting published resuls).
>
> Martin
>
> --
> 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 HomotopyTypeTheory+unsubscribe@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.

-- 
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 HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.