Discussion of Homotopy Type Theory and Univalent Foundations
 help / Atom feed
From: escardo.martin@gmail.com
To: Homotopy Type Theory <HomotopyTypeTheory@googlegroups.com>
Subject: Re: [HoTT] Injective types
Date: Tue, 30 Apr 2019 23:25:31 -0700 (PDT)
Message-ID: <7104f60a-7dba-4574-8629-860c0bc31967@googlegroups.com> (raw)
In-Reply-To: <CAOvivQzEOU1Zbk4k+A7SsEmnzn0F+a18Qy=R7e8zs4c+QEQCHA@mail.gmail.com>

[-- Attachment #1.1: Type: text/plain, Size: 3200 bytes --]

On 01/05/2019 03:50, Michael Shulman wrote:> 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.)
Right.

> However, it's not clear to me why cumulativity would be a problem.
In Agda each type gets a unique universe (or at most one universe) and
often (but not always) the system is able to infer them if we write
question marks "?" for them (but not always).

Cumulativity is not "on the nose" in the sense that from X : U_l you
would get X : U_m for m ≥ l. Instead, if you need to have (a copy of)
X in U_m, you need to use an explicit embedding U_l → U_m. (I only
ever used this embedding to show that U_l is a retract of U_m if we
assume propositional resizing.)

In practice, however, I never needed to use this embedding, as the
closure properties for universes work with more than one universe at a
time. For instance,

  if X:U_l and A : X → U_m, then Π X A : U_{max l m}.

With this kind of closure property, I haven't encountered the
practical need for cumulativity.

It is nice, in practice, that universes are uniquely
determined. Insted of thousands of level constraints, we have a
unique, small, (polymorphic) level assignment.

> 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?
In theory it wouldn't be a problem if it holds. However, if Agda did
have cumulativity, it would lose the unique-level assignment property
that I use to infer the levels of the results from my given levels of
the data. However, in the absence of a concrete proof assistant with
the option to enable and disable cumulativity, it is impossible to
perform experiments to confirm or reject this conjectural impression.

I consider the universe-level system of Agda to be excellent in
practice, and easy to use. Moreover, as I said, if I publish a
mathematical theorem developed in Agda, I think it is fair to the
reader to let them know what the universe level assignments are rather
than just say that they exist. In some cases, as injectivity, the
universe levels are crucial, and if we ignore them we get false
claims.

Best,
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.

[-- Attachment #1.2: Type: text/html, Size: 4066 bytes --]

  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
2019-05-01  6:25   ` escardo.martin [this message]
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=7104f60a-7dba-4574-8629-860c0bc31967@googlegroups.com \
    --to=escardo.martin@gmail.com \
    --cc=HomotopyTypeTheory@googlegroups.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