--- a/system-f.agda	Wed Mar 19 19:05:13 2014 +0700
+++ b/system-f.agda	Thu Mar 20 06:25:38 2014 +0700
@@ -131,6 +131,9 @@
 n2 : {l : Level } -> { X : Set l } -> Int {l} {X}
 n2 {l} {X} = \(x : X ) -> \(y : X -> X ) -> y (y x)
 
+n3 : {l : Level } -> { X : Set l } -> Int {l} {X}
+n3 {l} {X} = \(x : X ) -> \(y : X -> X ) -> y (y (y x))
+
 lemma13 : {l : Level } -> { X : Set l } -> S ( S ( Zero {l} {X}) )  ≡ n2 
 lemma13 {l} {X} = refl
 
@@ -138,5 +141,19 @@
 It {l} {U} u f t = t u f
 
 
+R : {l : Level} { U X : Set l}   -> U -> ( U -> Int {l} {X} ->  U ) -> Int -> U 
+R {l} {U} u v t =  π1 ( It {suc l} {U  ×  Int} (< u , Zero >) (λ (x : U × Int) →  < v (π1 x) (π2 x) , S (π2 x) > ) t ) 
+
+sum : {l : Level} {X : Set l} -> Int -> Int {l} {X} -> Int
+sum {l} {X} x y = R {l} {Int {l} {X}} y ( λ z -> λ w -> S z ) x
+
+mul : {l : Level} {X : Set l} -> Int -> Int -> Int
+mul x y = R Zero ( λ (z : Int) -> λ (w : Int) -> sum y z ) x
+
+fact : {l : Level} {X : Set l} -> Int -> Int
+fact  {l} {X} n = R  (S Zero) (λ ( z : Int) -> λ (w : Int) -> mul (S w) z ) n
 
 
+
+
+