```Discussion of Homotopy Type Theory and Univalent Foundations
help / Atom feed```
```From: escardo.martin@gmail.com
Subject: Re: [HoTT] Injective types
Date: Thu, 2 May 2019 13:46:22 -0700 (PDT)

[-- 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.

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

```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
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,

Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

switches of git-send-email(1):

git send-email \
--to=escardo.martin@gmail.com \

https://kernel.org/pub/software/scm/git/docs/git-send-email.html

```Discussion of Homotopy Type Theory and Univalent Foundations