--- a/systemF.agda	Tue Apr 08 13:34:26 2014 +0900
+++ b/systemF.agda	Tue Apr 08 15:29:46 2014 +0900
@@ -24,17 +24,17 @@
 
 -- Product
 
-_×_ : {i j k : Level} -> Set i -> Set j -> Set (i ⊔ j ⊔  (suc k))
-_×_  {i} {j} {k} U V = {X : Set k} -> (U -> V -> X) -> X
+_×_ : {l : Level} -> Set l -> Set l -> Set (suc l)
+_×_  {l}  U V = {X : Set l} -> (U -> V -> X) -> X
 
-<_,_> : {i j k : Level} -> {U : Set i} -> {V : Set j} -> U -> V -> (U × V)
-<_,_> {i} {j} {k} {U} {V} u v = \{X : Set k} -> \(x : U -> V -> X) -> x u v
+<_,_> : {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
 
-π1 : {i j : Level} -> {U : Set i} -> {V : Set j} -> (U × V) -> U
-π1  {i} {j} {U} {V} t = t {U} \(x : U) -> \(y : V) -> x
+π1 : {l : Level} -> {U : Set l} -> {V : Set l} -> (U × V) -> U
+π1  {l} {U} {V} t = t {U} \(x : U) -> \(y : V) -> x
 
-π2 : {i j : Level} ->  {U : Set i} -> {V : Set j} -> (U × V) -> V
-π2  {i} {j} {U} {V} t = t {V} \(x : U) -> \(y : V) -> y
+π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 = refl
@@ -93,17 +93,17 @@
 
 -- Int
 
-Int : {l : Level} -> Set (suc l)
-Int {l} = {X : Set l} -> X -> (X -> X) -> X
+Int : {l : Level} {X : Set l} -> Set l
+Int {l} {X} = X -> (X -> X) -> X
 
-O : {l : Level} -> Int
-O {l} = \{X : Set l} -> \(x : X) -> \(y : X -> X) -> x
+O : {l : Level} -> {X : Set l} -> Int 
+O {l} {X} =  \(x : X) -> \(y : X -> X) -> x
 
-S : {l : Level} -> Int -> Int
-S {l} t = \{X : Set l} -> \(x : X) -> \(y : X -> X) -> y (t {X} x y)
+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} u f
+It {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 = refl
@@ -111,6 +111,5 @@
 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 = refl
 
-g : {l : Level} -> {U : Set (suc l)} -> {f : U -> Int -> U} -> (U × Int) -> (U × Int)
-g {l} {U} {f} = \x -> \{X : Set l} -> <_,_> {suc l} {suc l} {l} {U} {Int} (f (π1 x) (π2 x)) (π2 x)
--- g {l} {U} {f} = \x -> < (f (π1 x) (π2 x)) , (π2 x) > -- {X} in _×_ removed by applied U. add \{X} lambda to type checking
\ No newline at end of file
+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) >
\ No newline at end of file