--- a/system-f.agda	Mon Mar 17 21:29:45 2014 +0700
+++ b/system-f.agda	Wed Mar 19 16:51:35 2014 +0700
@@ -41,17 +41,17 @@
 lemma05 : {u v : U} -> D u v F ≡  v
 lemma05 = refl
 
-_×_ : Set l -> Set l ->  Set (suc l)
-U × V =  {X : Set l} -> (U -> V -> X)  -> X 
+_×_ : {l : Level} -> Set l -> Set l ->  Set (suc l)
+_×_ {l} U V =  {X : Set l} -> (U -> V -> X)  -> X 
 
-<_,_> : {U V : Set l} -> U -> V -> (U ×  V) 
-<_,_> {U} {V} u v = \{X} -> \(x : U -> V -> X) -> x u v
+<_,_> : {l : Level} {U V : Set l} -> U -> V -> (U ×  V) 
+<_,_> {l} {U} {V} u v = \{X} -> \(x : U -> V -> X) -> x u v
 
-π1 : {U V : Set l} -> (U ×  V) -> U
-π1 {U} {V}  t = t {U} (\(x : U) -> \(y : V) -> x)
+π1 : {l : Level} {U V : Set l} -> (U ×  V) -> U
+π1 {l} {U} {V}  t = t {U} (\(x : U) -> \(y : V) -> x)
 
-π2 : {U V : Set l} -> (U ×  V) -> V
-π2 {U} {V}  t = t {V} (\(x : U) -> \(y : V) -> y)
+π2 : {l : Level} {U V : Set l} -> (U ×  V) -> V
+π2 {l} {U} {V}  t = t {V} (\(x : U) -> \(y : V) -> y)
 
 lemma06 : {U V : Set l } -> {u : U } -> {v : V} -> π1 ( < u , v > ) ≡  u
 lemma06 = refl
@@ -67,20 +67,29 @@
 
 -- Emp definision is still wrong...
 
-Emp  :  {l : Level} {X : Set l} ->  Set l
+Emp  :  ∀{l : Level} {X : Set l} ->  Set l
 Emp {l}  =  \{X : Set l} -> X
 
-ε :  {l l' : Level} (U : Set l)  ->  ((X : Set l) -> Emp {l} {X}) -> Emp {l} {U}
-ε U t =  t U
+ε :  {l : Level} {U : Set l}  -> Emp  -> Emp 
+ε {l} {U} t =  t {l} {U}
 
-lemma09 : {l l' : Level} {U : Set l} -> {t :  (X' : Set (suc l)) -> Emp }  -> ε U (ε Emp t) ≡ ε U ?
-lemma09 = refl
+lemma09 : {l : Level} {U : Set l} -> (t : Emp) -> ε 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 : {U V : Set l} -> {t :  U ×  V }  -> π1 ( ε ( U ×  V ) {!!} )  ≡ ε U {!!}
-lemma10 = refl
+lemma100 : {l : Level} {U V X : Set l} ->  (t : Emp ) -> Emp
+lemma100 {l} {U} {V} t = ε U t
+
+lemma101 : {l k : Level} {U V : Set l} ->  (t : Emp ) -> π1 (ε (U ×  V) t) ≡ ε U t
+lemma101 t = refl
 
--- lemma101 : {U V : Set l} -> {t :  U ×  V }  -> π2 ( ε {_} { U ×  V } t )  ≡ ε {_} {V} t
--- lemma101 = refl
+lemma102 : {l k : Level} {U V : Set l} ->  (t : Emp ) -> π2 (ε (U ×  V) t) ≡ ε V t
+lemma102 t = refl
+
+lemma103 : {l : Level} {U V : Set l} -> (u : U) -> (t : Emp) -> ε (U -> V) u ≡ ε V t
+lemma103 u t = refl
 
 _+_  : Set l -> Set l -> Set (suc l)
 U + V = {X : Set l} -> ( U -> X ) -> (V -> X) -> X