--- a/system-f.agda	Sun May 04 11:01:36 2014 +0900
+++ b/system-f.agda	Wed Dec 24 12:00:16 2014 +0900
@@ -1,10 +1,12 @@
+{-# OPTIONS --universe-polymorphism #-}
+
 open import Level
 open import Relation.Binary.PropositionalEquality
 
 module system-f  where
 
-Bool : {l : Level} (X : Set l) → Set l
-Bool = λ{l : Level} → λ(X : Set l) → X → X → X
+Bool : {l : Level} → Set l → Set l
+Bool {l} = λ(X : Set l) → X → X → X
 
 T : {l : Level} (X : Set l) → Bool X
 T X = λ(x y : X) → x
@@ -23,7 +25,7 @@
 
 _×_ : {l : Level} → Set l → Set l →  Set (suc l)
 _×_ {l} U V =  {X : Set l} → (U → V → X)  → X 
-
+ 
 <_,_> : {l : Level} {U V : Set l} → U → V → (U ×  V) 
 <_,_> {l} {U} {V} u v = λ{X} → λ(x : U → V → X) → x u v
 
@@ -57,33 +59,28 @@
 --lemma103 : {l : Level} {U V : Set l} → (u : U) → (t : Emp ) → (ε t (U → V) ) u ≡ ε t V 
 --lemma103 u t = e1 t u
 
-Emp  : {l : Level } → Set l → Set l
-Emp {l} = λ X → X
-
--- Emp is not allowed because Emp is not a Set of any level
+Emp  : {l : Level } → Set (suc l)
+Emp {l} = {X : Set l} → X 
 
--- ε :  {l : Level} (U : Set l)  → Emp → U
--- ε {l} U t =  t U
+-- ε :  {l : Level} {U : Set l} → Emp {l} → U
+-- ε {l} {U} t =  t U
 
--- lemma103 : {l : Level} {U V : Set l} → (u : U) → (t : Emp ) → (ε (U → V) t) u ≡ ε V t
+-- lemma103 : {l : Level} {U V : Set l} → (u : U) → (t : Emp {l} ) → (ε {l} {U → V} t) u ≡ ε {l} {V} t
 -- lemma103 u t = refl
 
--- lemma09 : {l : Level} {U : Set l}  → (t : Emp ) → ε U (ε Emp t) ≡ ε U t
+-- lemma09 : {l : Level} {U : Set l}  → (t : Emp ) → ε {l} {U} (ε {_} {Emp} t) ≡ ε {_} {U} t
 -- lemma09 t = refl
 
--- lemma10 :  {l : Level} {U V X : Set l} →  (t : Emp ) → U × V
--- lemma10  {l} {U} {V} t = ε (U ×  V) t
-
--- lemma10' : {l : Level} {U V X : Set l} →  (t : Emp ) → Emp
--- lemma10' {l} {U} {V} {X} t = ε (U ×  V) t 
+-- lemma10 :  {l : Level} {U V X : Set l} →  (t : Emp ) → U ×  V
+-- lemma10  {l} {U} {V} t = ε {suc l} {U ×  V} t
 
 -- lemma100 : {l : Level} {U V X : Set l} →  (t : Emp ) → Emp 
--- lemma100 {l} {U} {V} t = ε U t
+-- lemma100 {l} {U} {V} t = ε {_} {U} t
 
--- lemma101 : {l k : Level} {U V : Set l} →  (t : Emp ) → π1 (ε (U ×  V) t) ≡ ε U t
+-- lemma101 : {l : Level} {U V : Set l} →  (t : Emp ) → π1 (ε {suc l} {U ×  V} t) ≡ ε {l} {U} t
 -- lemma101 t = refl
 
--- lemma102 : {l k : Level} {U V : Set l} →  (t : Emp ) → π2 (ε (U ×  V) t) ≡ ε V t
+-- lemma102 : {l : Level} {U V : Set l} →  (t : Emp ) → π2 (ε {_} {U ×  V} t) ≡ ε {_} {V} t
 -- lemma102 t = refl