--- a/system-f.agda	Wed Mar 19 16:51:35 2014 +0700
+++ b/system-f.agda	Wed Mar 19 19:05:13 2014 +0700
@@ -70,26 +70,26 @@
 Emp  :  ∀{l : Level} {X : Set l} ->  Set l
 Emp {l}  =  \{X : Set l} -> X
 
-ε :  {l : Level} {U : Set l}  -> Emp  -> Emp 
-ε {l} {U} t =  t {l} {U}
+-- ε :  {l : Level} {U : Set l}  -> Emp  -> Emp 
+-- ε {l} {U} t =  t {l} {U}
 
-lemma09 : {l : Level} {U : Set l} -> (t : Emp) -> ε U (ε Emp t) ≡ ε U t
-lemma09 t = refl
+-- lemma09 : {l : Level} {U : Set l} -> (t : Emp) -> ε U (ε Emp t) ≡ ε U t
+-- lemma09 t = refl
 
-lemma10 : {l : Level} {U V X : Set l} ->  (t : Emp ) -> (U ×  V)
-lemma10 {l} {U} {V} t = ε (U ×  V) t
+-- lemma10 : {l : Level} {U V X : Set l} ->  (t : Emp ) -> (U ×  V)
+-- lemma10 {l} {U} {V} t = ε (U ×  V) t
 
-lemma100 : {l : Level} {U V X : Set l} ->  (t : Emp ) -> Emp
-lemma100 {l} {U} {V} t = ε U t
+-- lemma100 : {l : Level} {U V X : Set l} ->  (t : Emp ) -> Emp
+-- lemma100 {l} {U} {V} t = ε U t
 
-lemma101 : {l k : Level} {U V : Set l} ->  (t : Emp ) -> π1 (ε (U ×  V) t) ≡ ε U t
-lemma101 t = refl
+-- lemma101 : {l k : Level} {U V : Set l} ->  (t : Emp ) -> π1 (ε (U ×  V) t) ≡ ε U t
+-- lemma101 t = refl
 
-lemma102 : {l k : Level} {U V : Set l} ->  (t : Emp ) -> π2 (ε (U ×  V) t) ≡ ε V t
-lemma102 t = refl
+-- lemma102 : {l k : Level} {U V : Set l} ->  (t : Emp ) -> π2 (ε (U ×  V) t) ≡ ε V t
+-- lemma102 t = refl
 
-lemma103 : {l : Level} {U V : Set l} -> (u : U) -> (t : Emp) -> ε (U -> V) u ≡ ε V t
-lemma103 u t = refl
+-- lemma103 : {l : Level} {U V : Set l} -> (u : U) -> (t : Emp) -> ε (U -> V) u ≡ ε V t
+-- lemma103 u t = refl
 
 _+_  : Set l -> Set l -> Set (suc l)
 U + V = {X : Set l} -> ( U -> X ) -> (V -> X) -> X
@@ -110,14 +110,33 @@
 lemma12 u v s =  refl
 
 
+_××_ : {l : Level} -> Set (suc l) -> Set l ->  Set (suc l)
+_××_ {l} U V =  {X : Set l} -> (U -> V -> X)  -> X 
+
+<<_,_>> : {l : Level} {U : Set (suc l) } {V : Set l} -> U -> V -> (U  ××   V) 
+<<_,_>> {l} {U} {V} u v = \{X} -> \(x : U -> V -> X) -> x u v
 
 
+Int = \{l : Level } -> \{ X : Set l } -> X -> ( X -> X ) -> X
+
+Zero : {l : Level } -> { X : Set l } -> Int 
+Zero {l} {X} = \(x : X ) -> \(y : X -> X ) -> x
+
+S : {l : Level } -> { X : Set l } -> Int -> Int 
+S {l} {X} t = \(x : X) -> \(y : X -> X ) -> y ( t x y )
+
+n1 : {l : Level } -> { X : Set l } -> Int {l} {X}
+n1 {l} {X} = \(x : X ) -> \(y : X -> X ) -> y x
+
+n2 : {l : Level } -> { X : Set l } -> Int {l} {X}
+n2 {l} {X} = \(x : X ) -> \(y : X -> X ) -> y (y x)
+
+lemma13 : {l : Level } -> { X : Set l } -> S ( S ( Zero {l} {X}) )  ≡ n2 
+lemma13 {l} {X} = refl
+
+It : {l : Level} {U : Set l} -> U -> ( U -> U ) -> Int -> U
+It {l} {U} u f t = t u f
 
 
 
 
-
-
-
-
-