[Agda] Universes in Coq

[Vladimir Voevodsky]

On May 29, 2014, at 2:25 AM, Michael Shulman <shulman at sandiego.edu> wrote:

> Coq and the book use cumulativity, while Agda doesn't.

As I have discovered by talking to Hugo in the bus Coq actually *does not* use cumulativity. What it uses may be called "cumulative ambiguity" - a mechanism for hiding "casts" from one universe to another from the user.

Running the following code will give some idea of what Coq actually does:

(* *)

Set Printing Universes.

Definition U1 := Type.
Definition U2 : U1 := Type.

Print U1.
Print U2.

Variable A : U2.

Definition test1 := A -> A . 
Print test1.
Definition test11 := ( A : U1 ) -> A . 
Print test11.

Definition test2 := identity_refl test1 : identity test1 test11.
Set Printing Implicit.  
Print test2.

(* End of the ile universe_tests.v *)

The real expression which Coq has for "identity test1 test11" is as follows:

identity Unew ( cast ( prod ( cast U1 A ) A ) Unew ) ( cast ( prod A A ) Unew )

The fact that reflexivity is well typed in this identity shows that the casts are removed when terms are considered i.e. in Agda terminology "Coq uses "lifts" which compute".

Vladimir.