--- a/systemF.agda	Tue Apr 01 15:03:58 2014 +0900
+++ b/systemF.agda	Tue Apr 01 15:24:12 2014 +0900
@@ -65,13 +65,9 @@
 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
 
---Σ_,_ : X -> V -> Set l
---Σ_,_ {Vx} X V =  {Y : Set l} -> ({X : Set l} -> (Vx -> Y)) -> Y
-
-
-
 data V {l} (X : Set l) : Set l
   where
     v : X -> V X
@@ -81,3 +77,14 @@
 
 ⟨_,_⟩ : (U : Set l) -> (u : V U) -> Σ U , u
 ⟨_,_⟩ U u = \{Y : Set l} -> \(x : {X : Set l} -> (V X) -> Y) -> x {U} u
+
+∇_,_,_ :  {W : Set l} -> (X : Set l) -> { u : V X } -> X -> W -> Σ X , u  -> W
+∇_,_,_ {W} X {u} x w t = t {W} (\{X : Set l} -> \(x : V X) -> w)
+
+{-
+  proofs and types style
+  (∇ X , x , w ) ⟨ U , u ⟩ ≡ w
+-}
+
+lemma-nabla : {X W U : Set l} -> {x : X} -> {w : W} -> (∇_,_,_ {W} X {v x} x w) ⟨ X , (v x) ⟩ ≡ w
+lemma-nabla = refl