|
138
|
1 module record1 where
|
|
|
2
|
|
|
3 record _∧_ (A B : Set) : Set where
|
|
|
4 field
|
|
|
5 π1 : A
|
|
|
6 π2 : B
|
|
|
7
|
|
|
8 open _∧_
|
|
|
9
|
|
|
10 ex1 : {A B : Set} → ( A ∧ B ) → A
|
|
|
11 ex1 a∧b = {!!}
|
|
|
12
|
|
|
13 ex2 : {A B : Set} → ( A ∧ B ) → B
|
|
|
14 ex2 a∧b = {!!}
|
|
|
15
|
|
|
16 ex3 : {A B : Set} → A → B → ( A ∧ B )
|
|
|
17 ex3 a b = {!!}
|
|
|
18
|
|
|
19 ex4 : {A B : Set} → A → ( A ∧ A )
|
|
|
20 ex4 a = record { π1 = {!!} ; π2 = {!!} }
|
|
|
21
|
|
|
22 ex5 : {A B C : Set} → ( A ∧ B ) ∧ C → A ∧ (B ∧ C)
|
|
|
23 ex5 a∧b∧c = record { π1 = {!!} ; π2 = {!!} }
|
|
|
24
|
|
|
25 ex6 : {A B C : Set} → ( (A → B ) ∧ ( B → C) ) → A → C
|
|
|
26 ex6 = {!!}
|
|
|
27
|
