From: escardo.martin@gmail.com
To: Homotopy Type Theory <HomotopyTypeTheory@googlegroups.com>
Subject: Re: [HoTT] Injective types
Date: Thu, 2 May 2019 13:46:22 -0700 (PDT) [thread overview]
Message-ID: <2b380e43-8623-4900-b529-1e267155562f@googlegroups.com> (raw)
In-Reply-To: <CAOvivQwkwn1HDttRoOZk5d8fgEwdkO5x3Y7bpP=fFGbYG5s1BA@mail.gmail.com>
[-- Attachment #1.1: Type: text/plain, Size: 2704 bytes --]
On Wednesday, 1 May 2019 17:55:50 UTC+1, Michael Shulman wrote
>
>
> Yes, this is a good point in favor of Agda-style non-cumulative
> Russell universes over Coq-style cumulative Russell universes.
>
> But isn't there a middle ground with Tarski universes?
It would be nice to have such a middle ground, particularly because
formulating universe assumptions in each single definition and theorem is
unfamiliar in mathematical practice, and so "typical ambiguity" (pretending
there is only one universe) is potentially a good idea for many (or even
most) examples. But not in the paper I advertised in this thread.
Here I post an example when Giraud did precisely that, namely to assume two
arbitrary universes U and V, explaining why this is needed in that level of
generality after the formulation of a theorem and its proof, given to me by
Thierry Coquand:
https://www.cs.bham.ac.uk/~mhe/giraud-universes.pdf (photo of one page of
a book).
The book is “Cohmologie non abelienne” (1971,
https://www.springer.com/gp/book/9783540053071).
Suppose we
> have explicit lifting operators Lift : U_i -> U_{i+1}, so that as in
> Agda we have unique small polymorphic level assignments. But then
> suppose we have *definitional* equalities El(Lift(A)) == El(A). Then
> on the (rare) occasions when we do have to explicitly lift types from
> one universe to another,
I can confirm from a 26k line Agda development (with comments and repeated
blank lines removed in this counting of the number of lines) that not once
did I need to embed a universe into a larger universe, except when I wanted
to state the theorem that any universe is a retract of any larger universe
if one assumes the propositional resizing axiom (any proposition in a
universe U has an equivalent copy in any universe V). So I would say that
such situations are *extremely rare* in practice.
> we would get stronger cumulativity behavior.
> (And I could imagine a proof assistant that implements this and sugars
> away the El to look like Russell universes to the user.)
At the moment we can choose cumulativity (Coq) or non-cumulativity (Agda),
and there is no system that combines the virtues of Coq and Agda regarding
universe handling. (And I fear that such a system would potentially
multiply the vices of both. :-) )
M.
--
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: 3538 bytes --]
next prev parent reply other threads:[~2019-05-02 20:46 UTC|newest]
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
2019-05-01 16:55 ` Michael Shulman
2019-05-02 20:46 ` escardo.martin [this message]
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 publicly 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=2b380e43-8623-4900-b529-1e267155562f@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
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).