|
138
|
1 module lambda ( T : Set) ( t : T ) where
|
|
|
2
|
|
|
3
|
|
|
4 A→A : (A : Set ) → ( A → A )
|
|
|
5 A→A = λ A → λ ( a : A ) → a
|
|
|
6
|
|
|
7 lemma2 : (A : Set ) → A → A
|
|
|
8 lemma2 A a = {!!}
|
|
|
9
|
|
139
|
10 →intro : {A B : Set } → A → B → ( A → B )
|
|
|
11 →intro _ b = λ x → b
|
|
|
12
|
|
|
13 →elim : {A B : Set } → A → ( A → B ) → B
|
|
|
14 →elim a f = f a
|
|
138
|
15
|
|
|
16 ex1 : {A B : Set} → Set
|
|
|
17 ex1 {A} {B} = ( A → B ) → A → B
|
|
|
18
|
|
|
19 ex1' : {A B : Set} → Set
|
|
|
20 ex1' {A} {B} = A → B → A → B
|
|
|
21
|
|
|
22 ex2 : {A : Set} → Set
|
|
|
23 ex2 {A} = A → ( A → A )
|
|
|
24
|
|
141
|
25 proof2 : {A : Set } → ex2 {A}
|
|
|
26 proof2 = {!!}
|
|
138
|
27
|
|
141
|
28 ex3 : {A B : Set} → A → B
|
|
|
29 ex3 a = {!!}
|
|
138
|
30
|
|
141
|
31 ex4 : {A B : Set} → A → B → B
|
|
|
32 ex4 {A}{B} a b = {!!}
|
|
138
|
33
|
|
141
|
34 ex5 : {A B : Set} → A → B → A
|
|
|
35 ex5 = {!!}
|
|
138
|
36
|
|
|
37
|
|
|
38
|
|
141
|
39 postulate
|
|
|
40 Domain : Set
|
|
|
41 Range : Set
|
|
|
42 r : Range
|
|
|
43
|
|
|
44 ex6 : Domain → Range
|
|
138
|
45 ex6 a = {!!}
|
|
|
46
|
|
|
47 ex7 : {A : Set} → A → T
|
|
|
48 ex7 a = {!!}
|
|
|
49
|
|
|
50 ex11 : (A B : Set) → ( A → B ) → A → B
|
|
|
51 ex11 = {!!}
|
|
|
52
|
|
|
53 ex12 : (A B : Set) → ( A → B ) → A → B
|
|
|
54 ex12 = {!!}
|
|
|
55
|
|
|
56 ex13 : {A B : Set} → ( A → B ) → A → B
|
|
|
57 ex13 {A} {B} = {!!}
|
|
|
58
|
|
|
59 ex14 : {A B : Set} → ( A → B ) → A → B
|
|
|
60 ex14 x = {!!}
|
|
|
61
|
|
|
62
|
