changeset 2:bbf889402b64

wrote Sum Type
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Thu, 20 Mar 2014 17:30:00 +0900
parents eb55f604b970
children 26cf9069f70a
files systemF.agda
diffstat 1 files changed, 24 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- 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