The Coq mailing list

[Vladimir Voevodsky <vladimir AT ias.edu>]

Consider the following code:

Definition UU1 := Type .
Definition UU2 := Type .
Definition UU3 := Type .

(* The following two lines establish that UU1 : UU2 *)

Variable F : UU2 -> UU2 .
Variable a : F ( UU1 ) .

(* The following two lines establish that UU2 : UU3 and UU2 is a subtype of 
UU3 *)

Definition subuu2uu3 : UU2 -> UU3 := fun X : UU2 => X . 
Definition inuu2uu3 : UU3 := ( fun X0 : UU3 => X0 ) UU2 . 

(* The following code produces universe inconsistency by failing to recognize 
that the type of [ t ] is [ UU1 ] . *)
 
Definition test1 { T : UU3 } ( t : T ) := T .
Variable t : UU1 .
Variable b : F ( test1 t ) .

I think in this situation the inference algorithm should either complain that 
there is an ambiguity or infer UU1 as the type of t ( in general it should 
choose the lowest universe to which is known to t belong ) .

Vladimir.