Mercurial > hg > Members > tatsuki > proofsAndTypes

comparison and.agda @ 0:d9d5091eb899 draft default tip

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Try 'and' definition on agda
author tatsuki
date Tue, 04 Mar 2014 15:04:53 +0900
parents
children
comparison
equal deleted inserted replaced
-1:000000000000 0:d9d5091eb899
1 module and where
2
3 postulate U : Set
4 postulate V : Set
5 postulate T : Set
6
7 f : Set
8 f = U -> V
9
10 record _x_ (U V : Set) : Set where
11 field
12 pi1 : U
13 pi2 : V
14
15 postulate <_,_> : U -> V -> (U x V)
16
17 open _x_
18 postulate u : U
19 postulate v : V
20
21 uv : U x V
22 uv = < u , v >
23 pair : Set
24 pair = U x V
25
26
27 postulate t : T
28
29 x : T
30 x = t
31
32 data _==_ {A : Set} : A -> A -> Set where
33 refl : {x : A} -> x == x
34
35 lemma02 : U
36 lemma02 = pi1 (< u , v >)
37 lemma01 : (pi1 ( < u , v > )) == u
38 lemma01 = {!!}