--- a/system-f.agda	Sat Mar 15 10:15:54 2014 +0900
+++ b/system-f.agda	Sun Mar 16 17:51:55 2014 +0700
@@ -64,3 +64,49 @@
 
 -- lemma08 :  (t : U ×  V)  -> < π1 t  , π2 t > ≡ t
 -- lemma08 t = {!!}
+
+-- Emp definision is still wrong...
+
+Emp  =  \{X : Set l } -> X
+
+ε :  {X : Set l } -> ( Set l -> X ) ->  Emp  {X}
+ε {U} t = t U
+
+--lemma09 : {U : Set l} -> {t :  U }  -> ε {U} (ε {Emp} t)   ≡ ε {U} t
+--lemma09 = ?
+
+--lemma10 : {U V : Set l} -> (t :  U ×  V )  -> π1 ( ε  { U ×  V } t )  ≡ ε {U} t
+--lemma10 = ?
+
+_+_  : Set l -> Set l -> Set (suc l)
+U + V = {X : Set l} -> ( U -> X ) -> (V -> X) -> X
+
+ι1 : {U V : Set l} ->  U ->  U + V
+ι1 {U} {V} u = \{X} -> \(x : U -> X) -> \(y : V -> X ) -> x u
+
+ι2 : {U V : Set l} ->  V ->  U + V
+ι2 {U} {V} v = \{X} -> \(x : U -> X) -> \(y : V -> X ) -> y v
+
+-- δ's aguments should aware x as raw symbol
+
+δ : { U V R S : Set l } -> U -> U -> ( R + S ) -> U
+δ  {U} {V} {R} {S} u v t = t {U} (\(x : R) -> u ) ( \(y : S) -> v )
+
+lemma11 : { U V R S : Set l } -> (u v : U ) -> (r : R) -> δ  {U} {V} {R} {S} u v ( ι1 r )  ≡ u
+lemma11 u v r =  refl
+
+lemma12 : { U V R S : Set l } -> (u v : U ) -> (s : S) -> δ  {U} {V} {R} {S} u v ( ι2 s )  ≡ v
+lemma12 u v s =  refl
+
+
+
+
+
+
+
+
+
+
+
+
+