--- a/systemF.agda	Tue Mar 25 17:20:45 2014 +0900
+++ b/systemF.agda	Tue Apr 01 15:03:58 2014 +0900
@@ -67,14 +67,17 @@
 
 -- Existential
 
---Σ_,_ : {Vx : Set l} -> Set (suc l)
---Σ_,_ =  {Vx : Set l} -> (X : Set l) -> (V : {var : Set l} -> Vx) -> {Y : Set l} -> ({X : Set l} -> (Vx -> Y)) -> Y
+--Σ_,_ : X -> V -> Set l
+--Σ_,_ {Vx} X V =  {Y : Set l} -> ({X : Set l} -> (Vx -> Y)) -> Y
 
-Σ_,_ : {Vx : Set l} -> (X : Set l) -> (V : {var : Set l} -> Vx) -> Set (suc l)
-Σ_,_ {Vx} X V =  {Y : Set l} -> ({X : Set l} -> (Vx -> Y)) -> Y
+
 
---⟨_,_⟩ : {Vu : Set l} -> (U : Set l) -> (u : Vu) -> (Σ_,_ {Vu} U u)
---⟨_,_⟩ : {Vu : Set l} -> (U : Set l) -> (u : Vu) -> {Y : Set l} -> ({X : Set l} -> Set l -> Set l) -> Set l
+data V {l} (X : Set l) : Set l
+  where
+    v : X -> V X
 
-⟨_,_⟩ : {Vu : Set l} -> {V : {U : Set l}  -> Vu} -> (U : Set l) -> (u : Vu) -> (Σ_,_ {Vu} U V) 
-⟨_,_⟩ {Vu} {V} U u = \{Y : Set l} -> \(x : ({X : Set l} -> (Vu -> Y))) -> x {U} u
+Σ_,_ : (X : Set l) -> V X -> Set (suc l)
+Σ_,_ U u = {Y : Set l} -> ({X : Set l} -> (V X) -> Y) -> Y
+
+⟨_,_⟩ : (U : Set l) -> (u : V U) -> Σ U , u
+⟨_,_⟩ U u = \{Y : Set l} -> \(x : {X : Set l} -> (V X) -> Y) -> x {U} u