(* wlaczyc universe levels *)

Definition t1:=Type.
Definition t2:t1:=Type.

Print t1.
Print t2.
Print Universes.


Definition id (x:t2) := x.

Check id.

(* Check    id t1  . *)

Definition t3:=Type.
Definition t4:t3:=Type.

Definition w := t4 -> t2 : t1.

Print t3.
Print t4.

Print Universes.

Definition v := t2 -> t2 : t3.

Print Universes. 

Print Universes "univ.txt".

Definition z := t1 -> t4.

Print z.