--- a/system-f.agda	Sat May 03 11:46:05 2014 +0900
+++ b/system-f.agda	Sun May 04 11:01:36 2014 +0900
@@ -47,14 +47,21 @@
 
 -- Emp definision is still wrong...
 
-Emp  :  {l : Level} (U : Set l) →  Set l
-Emp {l} = λ( U : Set l) → U
+--record Emp {l : Level } : Set (suc l) where
+--   field 
+--      ε : (U : Set l ) → U
+--      e1 :  {U V : Set l} → (u : U) → (ε (U → V) ) u ≡ ε V
+--
+--open Emp
+
+--lemma103 : {l : Level} {U V : Set l} → (u : U) → (t : Emp ) → (ε t (U → V) ) u ≡ ε t V 
+--lemma103 u t = e1 t u
+
+Emp  : {l : Level } → Set l → Set l
+Emp {l} = λ X → X
 
 -- Emp is not allowed because Emp is not a Set of any level
 
--- t : Emp
--- t = ?
-
 -- ε :  {l : Level} (U : Set l)  → Emp → U
 -- ε {l} U t =  t U
 
@@ -136,8 +143,8 @@
 It : {l : Level} {U : Set l} → U → ( U → U ) → Int U → U
 It u f t = t u f
 
-ItInt : {l : Level} {X : Set l} → Int X → ( Int X → Int X ) → Int X → Int X
-ItInt {l} {X} u f t = λ z s → t (u z s) ( λ w → (f (λ z' s' → w )) z s )
+ItInt : {l : Level} {X : Set l} → Int X → (X → Int X ) → ( Int X → Int X ) → Int X → Int X
+ItInt {l} {X} u g f t = λ z s → t (u z s) ( λ (w : X) → (f (g w)) z s )
 
 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 ) 
@@ -150,7 +157,7 @@
 add x y = λ z s → x (y z s) s
 
 add'' : {l : Level} {X : Set l} → Int X → Int X → Int X
-add'' x y = ItInt y S x
+add'' x y = ItInt y (\w z s -> w )S x
 
 lemma22 : {l : Level} {X : Set l} ( x y : Int X ) → add x y  ≡ add'' x y
 lemma22 x y = refl
@@ -163,7 +170,7 @@
 mul {l} {X} x y = λ z s → x z ( λ w → y w s )
 
 mul'' : {l : Level } {X : Set l} → Int X → Int X → Int X
-mul'' {l} {X} x y = ItInt Zero (add'' x) y
+mul'' {l} {X} x y = ItInt Zero (\w z s -> w) (add'' x) y
 
 fact : {l : Level} {X : Set l} → Int _ → Int X
 fact  {l} {X} n = R (S Zero) (λ z → λ w → mul z (S w)) n
@@ -220,11 +227,11 @@
 l4 : {l : Level} {X X' : Set l} → Int X → List (Int X) (X')
 l4 x = Cons x (Cons x (Cons x Nil))
 
-ListIt : {l : Level} {U W : Set l} → W → ( U → W → W ) → List U W → W
+ListIt : {l : Level} {U X : Set l} → X → ( U → X → X ) → List U X → X
 ListIt w f t = t w f
 
-LListIt : {l : Level} {U W : Set l} → List U W  → ( U → List U W → List U W ) → List U W → List U W
-LListIt {l} {U} {W} w f t = λ x y → t (w x y) (λ x' y' → (f x' (λ x'' y'' → y' )) x y )
+LListIt : {l : Level} {U X : Set l} → List U X  → (X → List U X) → ( U → List U X → List U X ) → List U X → List U X
+LListIt {l} {U} {X} w g f t = λ x y → t (w x y) (λ (x' : U) (y' : X)  → (f x' (g y')) x y )
 
 -- Cdr : {l : Level} {U : Set l} {X : Set l} → List U X →  List U X
 -- Cdr w = λ x → λ y →  w x (λ x y   →  y) 
@@ -243,10 +250,10 @@
 Append' {_} {_} {X} x y = ListIt y Cons x    
 
 Append : {l : Level} {U : Set l} {X : Set l} → List U X → List U X → List U X
-Append x y = λ s t → x (y s t) t
+Append x y = λ n c → x (y n c) c
 
 Append'' : {l : Level} {U X : Set l} → List U X → List U X → List U X
-Append'' {_} {_} {X} x y = LListIt y Cons x   
+Append'' {_} {_} {X} x y = LListIt y (\e n c -> e) Cons x   
 
 lemma18 :{l : Level} {U : Set l} {X : Set l} → Append {_} {Int U} {X} l1 l2 ≡ Cons n1 (Cons n2 (Cons n1 Nil))
 lemma18 = refl
@@ -265,11 +272,11 @@
 lemma19 = refl
 
 Reverse' : {l : Level} {U : Set l} {X : Set l} → List U X → List U X
-Reverse' {l} {U} {X} x = LListIt Nil ( λ u w → Append w (Cons u Nil) ) x
+Reverse' {l} {U} {X} x = LListIt Nil (\e n c -> e) ( λ u w → Append w (Cons u Nil) ) x
 -- λ x x₁ y → x x₁ (λ x' y' → y')
 
 -- lemma19' :{l : Level} {U : Set l} {X : Set l} → Reverse' {_} {Int U} {X} l3 ≡ Cons n1 (Cons n2 (Cons n3 Nil))
--- lemma19' = {!!}
+-- lemma19' = refl
 
 Tree : {l : Level} → Set l → Set l → Set l
 Tree {l} = λ( U X : Set l)  → X → ( (U → X) →  X ) → X
@@ -280,7 +287,7 @@
 Collect : {l : Level} {U : Set l} {X : Set l} → (U → Tree U X ) → Tree U X
 Collect {l} {U} {X} f = λ(x : X) → λ(y : (U → X) → X) → y (λ(z : U) → f z x y )
 
-TreeIt : {l : Level} {U W X : Set l} → W → ( (U → W) → W ) → Tree U W → W
+TreeIt : {l : Level} {U X X : Set l} → X → ( (U → X) → X ) → Tree U X → X
 TreeIt w h t = t w h
 
 t0 :  {l : Level} {X X' : Set l} → Tree (Bool X) X'