--- a/systemF.agda	Tue Apr 29 22:27:25 2014 +0900
+++ b/systemF.agda	Wed Jun 11 16:41:01 2014 +0900
@@ -24,19 +24,19 @@
 
 -- Product
 
-_×_ : {l : Level} -> Set l -> Set l -> Set (suc l)
-_×_   {l}  U V = {X : Set l} -> (U -> V -> X) -> X
+_×_ : ∀ {l ll} -> Set l -> Set ll -> {lll : Level} -> Set (suc lll ⊔ (ll ⊔ l))
+_×_ {l} {ll} U V {lll} = {X : Set lll} -> (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
+<_,_> : ∀{l ll lll} -> {U : Set l} -> {V : Set ll} -> U -> V -> (U × V)
+<_,_> {l} {ll} {lll} {U} {V} u v = \{X : Set lll} -> \(x : U -> V -> X) -> x u v
 
-π1 : {l : Level} -> {U : Set l} -> {V : Set l} -> (U × V) -> U
-π1  {l} {U} {V} t = t {U} \(x : U) -> \(y : V) -> x
+π1 : ∀{l ll} -> {U : Set l} -> {V : Set ll} -> (U × V) -> U
+π1  {l} {ll} {U} {V} t = t {U} \(x : U) -> \(y : V) -> x
 
-π2 : {l : Level} ->  {U : Set l} -> {V : Set l} -> (U × V) -> V
-π2  {l} {U} {V} t = t {V} \(x : U) -> \(y : V) -> y
+π2 : ∀{l ll} ->  {U : Set l} -> {V : Set ll} -> (U × V) -> V
+π2  {l} {ll} {U} {V} t = t {V} \(x : U) -> \(y : V) -> y
 
-lemma-product : {l : Level} {U V : Set l} -> U -> V -> U × V
+lemma-product : {l ll : Level} {U V : Set l} -> U -> V -> (U × V) {ll}
 lemma-product u v = < u , v >
 
 lemma-product-pi1 : {l : Level} {U V : Set l} -> {u : U} -> {v : V} -> π1 (< u , v >) ≡ u
@@ -99,16 +99,16 @@
 
 -- Int
 
-Int : {l : Level} -> {X : Set l} -> Set l
+Int : ∀{l} -> {X : Set l} -> Set l
 Int {l} {X} = X -> (X -> X) -> X
 
 O : {l : Level} -> {X : Set l} -> Int
 O {l} {X} =  \(x : X) -> \(y : X -> X) -> x
 
-S : {l : Level} -> {X : Set l} -> Int -> Int
+S : ∀ {l X}  -> Int {l} {X} -> Int
 S {l} {X} t = \(x : X) -> \(y : X -> X) -> y (t x y)
 
-It : {l : Level} {U : Set l} -> (u : U) -> (U -> U) -> Int -> U
+It : ∀{l} {U : Set l} -> (u : U) -> (U -> U) -> Int -> U
 It {l} {U} u f t = t u f
 
 lemma-it-o : {l : Level} {U : Set l} -> {u : U} -> {f : U -> U} -> It u f O ≡ u
@@ -117,20 +117,28 @@
 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) >
+g : ∀{l ll U X} -> {f : U -> Int {l} {X} -> U} -> (U × Int) {l}-> (U × Int) {ll}
+g {l} {ll} {U} {X} {f} = \x -> < (f (π1 x) (π2 x)) , S (π2 x) >
 
-lemma-it-n : {l : Level} {U X : Set l} {u : U} {n : Int} {f : U -> Int -> U} -> (g {l} {U} {f} < u , n >) ≡ < f u n , S n > {X}
+lemma-g : ∀{l ll U X Y} {u : U} {n : Int} {f : U -> Int {l} {X} -> U} -> g {l} {ll} {U} {X} {f} < u , n > ≡  < f u n , S n > {Y}
+lemma-g = refl
+
+lemma-it-n : ∀{l ll U X Y} {u : U} {n : Int {l} {X}} {f : U -> Int {l} {X} -> U} -> (g {l} {ll} {U} {X} {f} < u , n >) ≡ < f u n , S n > {Y}
 lemma-it-n = refl
 
-R : {l : Level} -> {U : Set l} -> U -> (U -> Int -> U) -> Int -> U
-R {l} {U} u f t = π1 (It {suc l} {U × Int} < u , O > (g {_} {_} {f}) t)
+R : ∀{l U X} -> (u : U) -> (U -> Int {_} {X} -> U) -> Int -> U
+R  {l} {U} {X} u f t = π1 {l} (It {_} {U × Int} < u , O > (g {f = f}) t)
 
-lemma-R-O : {l : Level} {U : Set l} {u : U} {f : (U -> Int -> U)} -> R u f O ≡ u
+lemma-R-O : ∀{l U X} {u : U} {f : (U -> Int {l} {X} -> U)} -> R u f O ≡ u
 lemma-R-O = refl
 
-lemma-R-n : {l : Level} {U : Set l} {u : U} {f : (U -> Int -> U)} {n : Int} -> R u f (S n) ≡ f (R u f n) (n < u , O > (g {l} {U} {f}) (\u n ->  π2 < u , n > ))
-lemma-R-n = refl
+
+-- lemma-R-n : {l : Level} {U : Set l} {u : U} {f : (U -> Int -> U)} {n : Int} -> R u f (S n) ≡ f (R u f n) (n < u , O > (g {l} {U} {f}) (↑ n ->  π2 < u , n > ))
+
+-- not finished Proof lemma-R-n
+-- If applied g for Int. I think Int has type of (Int {?} {U × Int}).
+--lemma-R-n : ∀{u f}{n : Int} -> R u f (S n) ≡ f (R u f n) n
+--lemma-R-n = refl
 
 -- Proofs And Types Style lemma-R-n
 --lemma-R-n : {l : Level} {U : Set l} {u : U} {f : (U -> Int -> U)} {n : Int} -> R u f (S n) ≡ f (R u f n) n