Discussion of Homotopy Type Theory and Univalent Foundations
 help / Atom feed
From: Michael Shulman <shulman@sandiego.edu>
To: Martin Hotzel Escardo <escardo.martin@gmail.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: <9a1466e5-1c06-4ae2-abc5-d3fbfec5c851@googlegroups.com>

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.

  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' \
    --to=shulman@sandiego.edu \
    --cc=HomotopyTypeTheory@googlegroups.com \
    --cc=escardo.martin@gmail.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