--- a/systemF.agda	Thu Apr 10 16:26:28 2014 +0900
+++ b/systemF.agda	Tue Apr 15 17:20:52 2014 +0900
@@ -25,7 +25,7 @@
 -- Product
 
 _×_ : {l : Level} -> Set l -> Set l -> Set (suc l)
-_×_   {l} U V = {X : Set l} -> (U -> V -> X) -> X
+_×_   {l}  U V = {X : Set l} -> (U -> V -> X) -> X
 
 <_,_> : {l : Level} -> {U : Set l} -> {V : Set l} -> U -> V -> (U × V)
 <_,_> {l} {U} {V} u v = \{X : Set l} -> \(x : U -> V -> X) -> x u v
@@ -139,20 +139,20 @@
 
 -- List
 
-List : {l : Level} {ll : Level} -> (U : Set l) -> Set (suc ll ⊔ l)
-List {l} {ll} U = {X : Set ll} -> X -> (U -> X -> X) -> X
+List : {l ll : Level} -> (U : Set l) -> Set (l ⊔ (suc ll))
+List {l} {ll} U =  {X : Set ll} -> X -> (U -> X -> X) -> X
 
-nil : {l : Level} {ll : Level} {U : Set l} -> List U
-nil {l} {ll} {U} = \{X : Set ll} -> \(x : X) -> \(y : U -> X -> X) -> x
+nil : {l : Level} {U : Set l} {ll : Level} -> List U
+nil {l} {U} {ll} = \{X : Set ll} -> \(x : X) -> \(y : U -> X -> X) -> x
 
-cons : {l : Level} {ll : Level} {U : Set l} -> U -> List U -> List U
-cons {l} {ll} {U} u t = \{X : Set ll} -> \(x : X) -> \(y : U -> X -> X) -> y u (t {X} x y)
+cons : {l : Level} {U : Set l} {ll : Level}-> U -> List U -> List U
+cons {l} {U} {ll} u t = \{X : Set ll} -> \(x : X) -> \(y : U -> X -> X) -> y u (t {X} x y)
 
-ListIt : {l : Level} {ll : Level} {U : Set l} {W : Set ll} -> W -> (U -> W -> W) -> List U -> W
-ListIt {l} {ll} {U} {W} w f t = t {W} w f
+ListIt : {l : Level} {U : Set l} {ll : Level} {W : Set ll} -> W -> (U -> W -> W) -> List U -> W
+ListIt {l} {U} {ll} {W} w f t = t {W} w f
 
 -- (u1 u2 nil)
-lemma-list : {l : Level} {ll : Level} {U : Set l} {X : Set ll} {u1 u2 : U} {x : X} {y : U -> X -> X} -> (cons u1 (cons u2 nil)) x y ≡ y u1 (y u2 x)
+lemma-list : {l : Level} {U X : Set l} {u1 u2 : U} {x : X} {y : U -> X -> X} -> (cons u1 (cons u2 nil)) x y ≡ y u1 (y u2 x)
 lemma-list = refl
 
 lemma-list-it-nil : {l : Level} {U W : Set l} {w : W} {f : U -> W -> W} -> ListIt w f nil ≡ w
@@ -161,5 +161,16 @@
 lemma-list-it-cons : {l : Level} {U W : Set l} {u : U} {w : W} {f : U -> W -> W} {t : List U} -> ListIt w f (cons u t) ≡ f u (ListIt w f t)
 lemma-list-it-cons = refl
 
---lemma-list-nil-cons : {l : Level} {ll : Level} {U : Set l} {W : Set ll} {t : List U} -> ListIt {l} {?} {U} {List U} (nil {l} {ll} {U}) ({!!}) t ≡ t
---lemma-list-nil-cons = {!!}
\ No newline at end of file
+-- apply nil and cons to List U, return same list. but cannot justify type of cons and ListIt.
+-- if W = List U, cons has List U -> List (List U) -> (List U)
+
+--lemma-list-nil-cons : {l ll : Level} {U : Set ?} {X : Set ?} {t : List U} -> (ListIt {?} {?} {?} {List U} (nil) (cons) t) ≡ t
+--lemma-list-nil-cons = refl
+
+-- try concreate variable. has yellow.
+
+--li : {l ll : Level} {U : Set l} {u1 u2 : U} -> List {l} {ll} U
+--li {l} {ll} {U} {u1} {u2} = cons u1 (cons u2 nil) 
+
+--lemma-list-nil-cons-val : {l : Level} {U : Set l} -> (ListIt {l} {U} {suc l} {List U} (nil {l} {U}) (cons {l} {U} {l}) li) ≡ li
+--lemma-list-nil-cons-val = refl
\ No newline at end of file