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.