--- a/system-f.agda	Sat Mar 22 14:55:51 2014 +0700
+++ b/system-f.agda	Sat Mar 22 18:34:13 2014 +0700
@@ -133,19 +133,19 @@
 R : {l : Level} { U X : Set l}   -> U -> ( U -> Int X ->  U ) -> Int _ -> U 
 R {l} {U} {X} u v t =  π1 ( It {suc l} {U ×  Int X} (< u , Zero >) (λ (x : U × Int X) →  < v (π1 x) (π2 x) , S (π2 x) > ) t ) 
 
-add : {l : Level} {X : Set l} -> Int (Int X) -> Int X -> Int X
-add x y = It y S x
+add : {l : Level} {X : Set l} -> Int X -> Int X -> Int X
+add x y = \z t -> x (y z t) t
 
-mul : {l : Level } {X : Set l} -> Int (Int X) -> Int (Int X) -> Int X
+mul : {l : Level } {X : Set l} -> Int X -> Int (Int X) -> Int X
 mul {l} {X} x y = It Zero (add x) y
 
--- fact : {l : Level} {X : Set l} -> Int _ -> Int X
--- fact  {l} {X} n = R (S Zero) (λ (z : Int _) -> λ w -> mul z (S w) ) n
+fact : {l : Level} {X : Set l} -> Int _ -> Int X
+fact  {l} {X} n = R (S Zero) (λ z -> λ w -> mul z (S w) ) n
 
--- lemma13' : {l : Level} {X : Set l} -> fact {l} {X} n4 ≡ mul n4 ( mul n2 n3)
--- lemma13' = refl
+lemma13' : {l : Level} {X : Set l} -> fact {l} {X} n4 ≡ mul n4 ( mul n2 n3)
+lemma13' = refl
 
--- lemma14 : (x y : Int) -> mul x y  ≡ mul y x
+-- lemma14 : {l : Level} {X : Set l} -> (x y : Int X) -> mul x y  ≡ mul y x
 -- lemma14 x y = It {!!} {!!} {!!}
 
 lemma15 : {l : Level} {X : Set l} (x y : Int X) -> mul {l} {X} n2 n3  ≡ mul {l} {X} n3 n2