The Coq mailing list

[Georgi Guninski <guninski AT guninski.com>]

Using 2 Lemmas the inconsistency can be moved earlier and they break the
extended version of Daniel's paradox:

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

Lemma equ_1: forall a : UU1, exists b : UU2, a=b.
intro. eexists. intuition.
Qed.

Lemma equ_2: forall a : UU3, exists b : UU2, a=b.
intro. eexists. intuition.
Qed.
(* The following two lines establish that UU1 : UU2 *)

Variable F : UU2 -> UU2 .

(* Daniel's paradox can't be defined because of inconsistency
Inductive union_of_all_small_types : UU2 :=
| small_type_inc: forall {X:UU1},
  X -> union_of_all_small_types.
*)

Variable a : F ( UU1 ) .
(* Error: Universe inconsistency. *)





On Thu, Jun 30, 2011 at 04:18:50PM -0400, Vladimir Voevodsky wrote:
> 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.