From: Michael Shulman <firstname.lastname@example.org> To: Martin Hotzel Escardo <email@example.com> Cc: Homotopy Type Theory <HomotopyTypeTheory@googlegroups.com> Subject: Re: [HoTT] Injective types Date: Tue, 30 Apr 2019 19:50:49 -0700 Message-ID: <CAOvivQzEOU1Zbk4k+A7SsEmnzn0F+a18Qy=R7e8zs4c+QEQCHA@mail.gmail.com> (raw) In-Reply-To: <firstname.lastname@example.org> 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 <email@example.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 HomotopyTypeTheoryfirstname.lastname@example.org. > 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 HomotopyTypeTheoryemail@example.com. For more options, visit https://groups.google.com/d/optout.
next prev parent reply index Thread overview: 11+ messages / expand[flat|nested] mbox.gz Atom feed top 2019-04-30 23:05 escardo.martin 2019-05-01 2:50 ` Michael Shulman [this message] 2019-05-01 6:25 ` escardo.martin 2019-05-01 16:55 ` Michael Shulman 2019-05-02 20:46 ` escardo.martin 2019-05-03 11:45 ` Michael Shulman 2019-05-03 13:25 ` Kenji Maillard 2019-05-03 18:23 ` Thierry Coquand 2019-05-07 12:42 ` Nils Anders Danielsson 2019-05-07 13:51 ` Andreas Nuyts 2019-05-07 22:06 ` Martín Hötzel Escardó
Reply instructions: You may reply publically to this message via plain-text email using any one of the following methods: * Save the following mbox file, import it into your mail client, and reply-to-all from there: mbox Avoid top-posting and favor interleaved quoting: https://en.wikipedia.org/wiki/Posting_style#Interleaved_style * Reply using the --to, --cc, and --in-reply-to switches of git-send-email(1): git send-email \ --in-reply-to='CAOvivQzEOU1Zbk4k+A7SsEmnzn0F+a18Qy=R7e8zs4c+QEQCHA@mail.gmail.com' \ --firstname.lastname@example.org \ --cc=HomotopyTypeTheory@googlegroups.com \ --email@example.com \ /path/to/YOUR_REPLY https://kernel.org/pub/software/scm/git/docs/git-send-email.html * If your mail client supports setting the In-Reply-To header via mailto: links, try the mailto: link
Discussion of Homotopy Type Theory and Univalent Foundations Archives are clonable: git clone --mirror http://inbox.vuxu.org/hott Newsgroup available over NNTP: nntp://inbox.vuxu.org/vuxu.archive.hott AGPL code for this site: git clone https://public-inbox.org/ public-inbox