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: Thu, 2 May 2019 13:46:22 -0700 (PDT)
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 --]

  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
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 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=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

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