--- a/systemF.agda	Tue Apr 08 16:31:08 2014 +0900
+++ b/systemF.agda	Tue Apr 08 16:42:52 2014 +0900
@@ -1,7 +1,7 @@
 open import Level
 open import Relation.Binary.PropositionalEquality
 
-module systemF {l : Level}  where
+module systemF where
 
 -- Bool
 
@@ -25,7 +25,7 @@
 -- Product
 
 _×_ : {l : Level} -> Set l -> Set l -> Set (suc l)
-_×_  {l}  U V = {X : Set l} -> (U -> V -> X) -> X
+_×_   {l} U V = {X : Set l} -> (U -> V -> X) -> X
 
 <_,_> : {l : Level} -> {U : Set l} -> {V : Set l} -> U -> V -> (U × V)
 <_,_> {l} {U} {V} u v = \{X : Set l} -> \(x : U -> V -> X) -> x u v
@@ -36,10 +36,10 @@
 π2 : {l : Level} ->  {U : Set l} -> {V : Set l} -> (U × V) -> V
 π2  {l} {U} {V} t = t {V} \(x : U) -> \(y : V) -> y
 
-lemma-product-pi1 : {U V : Set l} -> {u : U} -> {v : V} -> π1 (< u , v >) ≡ u
+lemma-product-pi1 : {l : Level} {U V : Set l} -> {u : U} -> {v : V} -> π1 (< u , v >) ≡ u
 lemma-product-pi1 = refl
 
-lemma-product-pi2 : {U V : Set l} -> {u : U} -> {v : V} -> π2 (< u , v >) ≡ v
+lemma-product-pi2 : {l : Level} {U V : Set l} -> {u : U} -> {v : V} -> π2 (< u , v >) ≡ v
 lemma-product-pi2 = refl
 
 -- Empty
@@ -50,19 +50,19 @@
 _+_ : {l : Level} ->  Set l -> Set l -> Set (suc l)
 _+_ {l} U V = {X : Set  l} -> (U -> X) -> (V -> X) -> X
 
-ι1 :  {U V : Set l} -> U -> (U + V)
-ι1  {U} {V} u =  \{X : Set l} -> \(x : U -> X) -> \(y : V -> X) -> x u
+ι1 :  {l : Level} {U V : Set l} -> U -> (U + V)
+ι1  {l} {U} {V} u =  \{X : Set l} -> \(x : U -> X) -> \(y : V -> X) -> x u
 
-ι2 :  {U V : Set l} -> V -> (U + V)
-ι2  {U} {V} v =  \{X : Set l} -> \(x : U -> X) -> \(y : V -> X) -> y v
+ι2 : {l : Level} {U V : Set l} -> V -> (U + V)
+ι2  {l} {U} {V} v =  \{X : Set l} -> \(x : U -> X) -> \(y : V -> X) -> y v
 
 δ : {l : Level} -> {U V : Set l} -> {X : Set l} -> (U -> X) -> (V -> X) -> (U + V) -> X
 δ {l} {U} {V} {X} u v t = t {X} u v
 
-lemma-sum-iota1 : {U V X R : Set l} -> {u : U} -> {ux : (U -> X)} -> {vx : (V -> X)} -> δ ux vx (ι1 u) ≡ ux u
+lemma-sum-iota1 : {l : Level} {U V X R : Set l} -> {u : U} -> {ux : (U -> X)} -> {vx : (V -> X)} -> δ ux vx (ι1 u) ≡ ux u
 lemma-sum-iota1 = refl
 
-lemma-sum-iota2 : {U V X R : Set l} -> {v : V} -> {ux : (U -> X)} -> {vx : (V -> X)} -> δ ux vx (ι2 v) ≡ vx v
+lemma-sum-iota2 : {l : Level} {U V X R : Set l} -> {v : V} -> {ux : (U -> X)} -> {vx : (V -> X)} -> δ ux vx (ι2 v) ≡ vx v
 lemma-sum-iota2 = refl
 
 
@@ -72,14 +72,14 @@
   where
     v : X -> V X
 
-Σ_,_ : (X : Set l) -> V X -> Set (suc l)
-Σ_,_ U u = {Y : Set l} -> ({X : Set l} -> (V X) -> Y) -> Y
+Σ_,_ : {l : Level} (X : Set l) -> V X -> Set (suc l)
+Σ_,_ {l} U u = {Y : Set l} -> ({X : Set l} -> (V X) -> Y) -> Y
 
-⟨_,_⟩ : (U : Set l) -> (u : V U) -> Σ U , u
-⟨_,_⟩ U u = \{Y : Set l} -> \(x : {X : Set l} -> (V X) -> Y) -> x {U} u
+⟨_,_⟩ : {l : Level} (U : Set l) -> (u : V U) -> Σ U , u
+⟨_,_⟩ {l} U u = \{Y : Set l} -> \(x : {X : Set l} -> (V X) -> Y) -> x {U} u
 
-∇_,_,_ :  {W : Set l} -> (X : Set l) -> { u : V X } -> X -> W -> Σ X , u  -> W
-∇_,_,_ {W} X {u} x w t = t {W} (\{X : Set l} -> \(x : V X) -> w)
+∇_,_,_ :  {l : Level} {W : Set l} -> (X : Set l) -> { u : V X } -> X -> W -> Σ X , u  -> W
+∇_,_,_ {l} {W} X {u} x w t = t {W} (\{X : Set l} -> \(x : V X) -> w)
 
 {-
   lemma-nabla on proofs and types
@@ -87,7 +87,7 @@
   w[U/X][u/x^[U/X]]
 -}
 
-lemma-nabla : {X W : Set l} -> {x : X} -> {w : W} -> (∇_,_,_ {W} X {v x} x w) ⟨ X , (v x) ⟩ ≡ w
+lemma-nabla : {l : Level} {X W : Set l} -> {x : X} -> {w : W} -> (∇_,_,_ {l} {W} X {v x} x w) ⟨ X , (v x) ⟩ ≡ w
 lemma-nabla = refl
 
 
@@ -102,17 +102,17 @@
 S : {l : Level} -> {X : Set l} -> Int -> Int
 S {l} {X} t = \(x : X) -> \(y : X -> X) -> y (t x y)
 
-It : {U : Set l} -> (u : U) -> (U -> U) -> Int -> U
-It {U} u f t = t u f
+It : {l : Level} {U : Set l} -> (u : U) -> (U -> U) -> Int -> U
+It {l} {U} u f t = t u f
 
-lemma-it-o : {U : Set l} -> {u : U} -> {f : U -> U} -> It u f O ≡ u
+lemma-it-o : {l : Level} {U : Set l} -> {u : U} -> {f : U -> U} -> It u f O ≡ u
 lemma-it-o = refl
 
-lemma-it-s-o : {U : Set l} -> {u : U} -> {f : U -> U} -> {t : Int} -> It u f (S t) ≡ f (It u f t)
+lemma-it-s-o : {l : Level} {U : Set l} -> {u : U} -> {f : U -> U} -> {t : Int} -> It u f (S t) ≡ f (It u f t)
 lemma-it-s-o = refl
 
 g : {l : Level} -> {U : Set l} -> {f : U -> Int {l} {U} -> U} -> (U × Int) -> (U × Int)
 g {l} {U} {f} = \x -> < (f (π1 x) (π2 x)) , S (π2 x) >
 
-lemma-it : {l : Level} {U : Set l} {u : U} {n : Int} {f : U -> Int -> U} -> g {l} {U} {f} < u , n > ≡ < f u n , S n >
-lemma-it = refl
+lemma-it-n : {l : Level} {U : Set l} {u : U} {n : Int} {f : U -> Int -> U} -> g {l} {U} {f} < u , n > ≡ < f u n , S n >
+lemma-it-n = refl
\ No newline at end of file