|
138
|
1 module record1 where
|
|
|
2
|
|
|
3 record _∧_ (A B : Set) : Set where
|
|
|
4 field
|
|
|
5 π1 : A
|
|
|
6 π2 : B
|
|
|
7
|
|
266
|
8 ex0 : {A B : Set} → A ∧ B → A
|
|
|
9 ex0 = _∧_.π1
|
|
|
10
|
|
|
11 ex1 : {A B : Set} → ( A ∧ B ) → A
|
|
|
12 ex1 a∧b = _∧_.π1 a∧b
|
|
|
13
|
|
138
|
14 open _∧_
|
|
|
15
|
|
266
|
16 ex0' : {A B : Set} → A ∧ B → A
|
|
|
17 ex0' = π1
|
|
|
18
|
|
|
19 ex1' : {A B : Set} → ( A ∧ B ) → A
|
|
|
20 ex1' a∧b = π1 a∧b
|
|
138
|
21
|
|
|
22 ex2 : {A B : Set} → ( A ∧ B ) → B
|
|
|
23 ex2 a∧b = {!!}
|
|
|
24
|
|
|
25 ex3 : {A B : Set} → A → B → ( A ∧ B )
|
|
|
26 ex3 a b = {!!}
|
|
|
27
|
|
|
28 ex4 : {A B : Set} → A → ( A ∧ A )
|
|
|
29 ex4 a = record { π1 = {!!} ; π2 = {!!} }
|
|
|
30
|
|
|
31 ex5 : {A B C : Set} → ( A ∧ B ) ∧ C → A ∧ (B ∧ C)
|
|
|
32 ex5 a∧b∧c = record { π1 = {!!} ; π2 = {!!} }
|
|
|
33
|
|
266
|
34 --
|
|
|
35 -- [(A → B ) ∧ ( B → C) ]₁
|
|
|
36 -- ──────────────────────────────────── π1
|
|
|
37 -- [(A → B ) ∧ ( B → C) ]₁ (A → B ) [A]₂
|
|
|
38 -- ──────────────────────────── π2 ─────────────────────── λ-elim
|
|
|
39 -- ( B → C) B
|
|
|
40 -- ─────────────────────────────────────────── λ-elim
|
|
|
41 -- C
|
|
|
42 -- ─────────────────────────────────────────── λ-intro₂
|
|
|
43 -- A → C
|
|
|
44 -- ─────────────────────────────────────────── λ-intro₁
|
|
|
45 -- ( (A → B ) ∧ ( B → C) ) → A → C
|
|
|
46
|
|
138
|
47 ex6 : {A B C : Set} → ( (A → B ) ∧ ( B → C) ) → A → C
|
|
266
|
48 ex6 x a = {!!}
|
|
138
|
49
|
|
266
|
50 ex6' : {A B C : Set} → (A → B ) → ( B → C) → A → C
|
|
|
51 ex6' = {!!}
|
|
|
52
|
