--- a/systemF.agda	Thu Mar 20 17:30:00 2014 +0900
+++ b/systemF.agda	Mon Mar 24 20:12:59 2014 +0900
@@ -64,3 +64,18 @@
 
 lemma-sum-iota2 : {U V X R : Set l} -> {v : V} -> {ux : (U -> X)} -> {vx : (V -> X)} -> δ ux vx (ι2 v) ≡ vx v
 lemma-sum-iota2 = refl
+
+-- Existential
+
+--Σ_,_ : {l : Level} -> (X : Set l) -> (V : Set l) -> {Y : Set l} -> {X : Set l} -> {VX : (Set -> Set )} -> Set l
+--Σ_,_ : Set l -> Set l -> {Y : Set l} -> (Set l ->  Y)  -> Y
+--Σ_,_ : Set -> Set -> {Y : Set l} -> ? -> ?
+--Σ_,_  X V =  \{Y : Set l} -> (\(V : Set) -> Y) ->  Y
+
+Σ_,_ :  Set l -> (V : Set l) -> {v : V} -> {Y : Set l} -> (V -> Y) -> Y
+Σ_,_ X V {v} = \{Y : Set l} -> \(vy : V -> Y) -> vy v
+
+--⟨_,_⟩ : (U : Set l) -> (u : U) -> (Σ U , V)
+--⟨_,_⟩ : Set l -> ? -> {Y : Set l} -> ? -> ? -> ?
+--⟨_,_⟩ U u = \{Y : Set l} -> (x : (\{X} -> \(v : V) -> y)) -> x U u
+--⟨_,_⟩ U u = \{Y : Set l} -> \(x : (\{X : Set l} -> (VY : (V -> Y)))) ->  x U u