# HG changeset patch
# User Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
# Date 1395304200 -32400
# Node ID bbf889402b642f92de2738c7f367350c5c3eb219
# Parent  eb55f604b970dc41b8d89fa785101205fcd6dfb0
wrote Sum Type

diff -r eb55f604b970 -r bbf889402b64 systemF.agda
--- a/systemF.agda	Thu Mar 20 14:50:35 2014 +0900
+++ b/systemF.agda	Thu Mar 20 17:30:00 2014 +0900
@@ -40,4 +40,27 @@
 lemma-product-pi1 = refl
 
 lemma-product-pi2 : {U V : Set l} -> {u : U} -> {v : V} -> π2 (< u , v >) ≡ v
-lemma-product-pi2 = refl
\ No newline at end of file
+lemma-product-pi2 = refl
+
+-- Empty
+
+
+-- Sum
+
+_+_ : {l : Level} ->  Set l -> Set l -> Set (suc l)
+_+_ {l} U V = {X : Set  l} -> (U -> X) -> (V -> X) -> X
+
+ι1 :  {U V : Set l} -> U -> (U + V)
+ι1  {U} {V} u =  \{X : Set l} -> \(x : U -> X) -> \(y : V -> X) -> x u
+
+ι2 :  {U V : Set l} -> V -> (U + V)
+ι2  {U} {V} v =  \{X : Set l} -> \(x : U -> X) -> \(y : V -> X) -> y v
+
+δ : {l : Level} -> {U V : Set l} -> {X : Set l} -> (U -> X) -> (V -> X) -> (U + V) -> X
+δ {l} {U} {V} {X} u v t = t {X} u v
+
+lemma-sum-iota1 : {U V X R : Set l} -> {u : U} -> {ux : (U -> X)} -> {vx : (V -> X)} -> δ ux vx (ι1 u) ≡ ux u
+lemma-sum-iota1 = refl
+
+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