Mercurial > hg > Members > atton > agda > systemF

annotate systemF.agda @ 0:b7c49383e386

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Bool and Product in System F
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Thu, 20 Mar 2014 14:49:33 +0900
parents
children bbf889402b64
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
0
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 open import Level
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2 open import Relation.Binary.PropositionalEquality
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 module systemF {l : Level} where
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6 -- Bool
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
8 Bool = \{l : Level} -> {X : Set l} -> X -> X -> X
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 T : Bool
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 T = \{X : Set} -> \(x : X) -> \y -> x
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 F : Bool
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 F = \{X : Set} -> \x -> \(y : X) -> y
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
15
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
16 D : {X : Set} -> (U V : X) -> Bool -> X
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17 D {X} u v bool = bool {X} u v
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
18
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
19 lemma-bool-t : {X : Set} -> {u v : X} -> D {X} u v T ≡ u
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
20 lemma-bool-t = refl
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
21
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
22 lemma-bool-f : {X : Set} -> {u v : X} -> D {X} u v F ≡ v
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
23 lemma-bool-f = refl
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
24
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
25 -- Product
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
26
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
27 _×_ : {l : Level} -> Set l -> Set l -> Set (suc l)
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
28 _×_ {l} U V = {X : Set l} -> (U -> V -> X) -> X
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
29
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
30 <_,_> : {l : Level} -> {U V : Set l} -> U -> V -> (U × V)
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
31 <_,_> {l} {U} {V} u v = \{X} -> \(x : U -> V -> X) -> x u v
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
32
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
33 π1 : {U V : Set l} -> (U × V) -> U
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
34 π1 {U} {V} t = t {U} \(x : U) -> \(y : V) -> x
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
35
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
36 π2 : {U V : Set l} -> (U × V) -> V
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
37 π2 {U} {V} t = t {V} \(x : U) -> \(y : V) -> y
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
38
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
39 lemma-product-pi1 : {U V : Set l} -> {u : U} -> {v : V} -> π1 (< u , v >) ≡ u
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
40 lemma-product-pi1 = refl
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
41
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
42 lemma-product-pi2 : {U V : Set l} -> {u : U} -> {v : V} -> π2 (< u , v >) ≡ v
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
43 lemma-product-pi2 = refl