Mercurial > hg > Members > atton > agda > systemF
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