Mercurial > hg > Members > atton > agda > systemF
comparison systemF.agda @ 2:bbf889402b64
wrote Sum Type
author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
---|---|
date | Thu, 20 Mar 2014 17:30:00 +0900 (2014-03-20) |
parents | b7c49383e386 |
children | 26cf9069f70a |
comparison
equal
deleted
inserted
replaced
1:eb55f604b970 | 2:bbf889402b64 |
---|---|
39 lemma-product-pi1 : {U V : Set l} -> {u : U} -> {v : V} -> π1 (< u , v >) ≡ u | 39 lemma-product-pi1 : {U V : Set l} -> {u : U} -> {v : V} -> π1 (< u , v >) ≡ u |
40 lemma-product-pi1 = refl | 40 lemma-product-pi1 = refl |
41 | 41 |
42 lemma-product-pi2 : {U V : Set l} -> {u : U} -> {v : V} -> π2 (< u , v >) ≡ v | 42 lemma-product-pi2 : {U V : Set l} -> {u : U} -> {v : V} -> π2 (< u , v >) ≡ v |
43 lemma-product-pi2 = refl | 43 lemma-product-pi2 = refl |
44 | |
45 -- Empty | |
46 | |
47 | |
48 -- Sum | |
49 | |
50 _+_ : {l : Level} -> Set l -> Set l -> Set (suc l) | |
51 _+_ {l} U V = {X : Set l} -> (U -> X) -> (V -> X) -> X | |
52 | |
53 ι1 : {U V : Set l} -> U -> (U + V) | |
54 ι1 {U} {V} u = \{X : Set l} -> \(x : U -> X) -> \(y : V -> X) -> x u | |
55 | |
56 ι2 : {U V : Set l} -> V -> (U + V) | |
57 ι2 {U} {V} v = \{X : Set l} -> \(x : U -> X) -> \(y : V -> X) -> y v | |
58 | |
59 δ : {l : Level} -> {U V : Set l} -> {X : Set l} -> (U -> X) -> (V -> X) -> (U + V) -> X | |
60 δ {l} {U} {V} {X} u v t = t {X} u v | |
61 | |
62 lemma-sum-iota1 : {U V X R : Set l} -> {u : U} -> {ux : (U -> X)} -> {vx : (V -> X)} -> δ ux vx (ι1 u) ≡ ux u | |
63 lemma-sum-iota1 = refl | |
64 | |
65 lemma-sum-iota2 : {U V X R : Set l} -> {v : V} -> {ux : (U -> X)} -> {vx : (V -> X)} -> δ ux vx (ι2 v) ≡ vx v | |
66 lemma-sum-iota2 = refl |