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