--- a/systemF.agda	Mon Apr 07 11:06:28 2014 +0900
+++ b/systemF.agda	Tue Apr 08 12:36:49 2014 +0900
@@ -24,17 +24,17 @@
 
 -- Product
 
-_×_ : {l : Level} -> Set l -> Set l -> Set (suc l)
-_×_ {l} U V = {X : Set l} -> (U -> V -> X) -> X
+_×_ : {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} -> {U V : Set l} -> U -> V -> (U × V)
-<_,_> {l} {U} {V} u v = \{X} -> \(x : U  -> V -> X) -> x u v
+<_,_> : {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
 
-π1 : {U V : Set l} -> (U × V) -> U
-π1 {U} {V} t = t {U} \(x : U) -> \(y : V) -> x
+π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
 
-π2 : {U V : Set l} -> (U × V) -> V
-π2 {U} {V} t = t {V} \(x : U) -> \(y : V) -> y
+π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
 
 lemma-product-pi1 : {U V : Set l} -> {u : U} -> {v : V} -> π1 (< u , v >) ≡ u
 lemma-product-pi1 = refl
@@ -93,19 +93,31 @@
 
 -- Int
 
-Int = {X : Set} -> X -> (X -> X) -> X
-
-O : Int
-O = \{X : Set} -> \(x : X) -> \(y : X -> X) -> x
+Int : {l : Level} -> Set (suc l)
+Int {l} = {X : Set l} -> X -> (X -> X) -> X
 
-S : Int -> Int
-S t = \{X : Set} -> \(x : X) -> \(y : X -> X) -> y (t {X} x y)
+O : {l : Level} -> Int
+O {l} = \{X : Set l} -> \(x : X) -> \(y : X -> X) -> x
 
-It : {U : Set} -> (u : U) -> (U -> U) -> Int -> U
+S : {l : Level} -> Int -> Int
+S {l} t = \{X : Set l} -> \(x : X) -> \(y : X -> X) -> y (t {X} x y)
+
+It : {U : Set l} -> (u : U) -> (U -> U) -> Int -> U
 It {U} u f t = t {U} u f
 
-lemma-it-o : {U : Set} -> {u : U} -> {f : U -> U} -> It u f O ≡ u
+lemma-it-o : {U : Set l} -> {u : U} -> {f : U -> U} -> It u f O ≡ u
 lemma-it-o = refl
 
-lemma-it-s-o : {U : Set} -> {u : U} -> {f : U -> U} -> {t : Int} -> It u f (S t) ≡ f (It u f t)
-lemma-it-s-o = refl
\ No newline at end of file
+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) >