|
0
|
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 = {!!} |
