--- a/systemF.agda	Tue Apr 08 12:36:49 2014 +0900
+++ b/systemF.agda	Tue Apr 08 13:31:25 2014 +0900
@@ -24,11 +24,11 @@
 
 -- Product
 
-_×_ : {i j k : Level}  -> Set i -> Set j -> Set (i ⊔ j ⊔ (suc k))
+_×_ : {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
 
 <_,_> : {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
+<_,_> {i} {j} {k} {U} {V} u v = \{X : Set k} -> \(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
@@ -111,13 +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
 
--- U only
---g : {i : Level} -> {U : Set (suc i)} -> {f : U -> Int {i} -> U} -> (U × (Int {i})) -> U
---g {i} {U} {f} = \(x : (U × Int {i})) -> (f (π1 x) (π2 x))
-
--- Int Only
---g : {i : Level} -> {U : Set (suc i)} -> {f : U -> Int {i} -> U} -> (U × (Int {i})) -> Int {i}
---g {i} {U} {f} = \(x : (U × Int {i})) -> (π2 x)
-
-g : {i : Level} -> {U : Set (suc i)} -> {f : U -> Int {i} -> U} -> (U × (Int {i})) -> U × Int {i}
-g {i} {U} {f} = \(x : (U × Int {i})) -> < (f (π1 x)  (π2 x)) , (π2 x) >
+g : {l : Level} -> {U : Set (suc l)} -> {f : U -> Int -> U} -> (U × Int) -> (_×_ {suc l} {suc l} U Int)
+g {l} {U} {f} = \x -> \{X : Set l} -> <_,_> {suc l} {suc l} {l} {U} {Int} (f (π1 x) (π2 x)) (π2 x)
\ No newline at end of file