|
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
|
|
|
25 ex3 : {A B : Set} → Set
|
|
|
26 ex3 {A}{B} = A → B
|
|
|
27
|
|
|
28 ex4 : {A B : Set} → Set
|
|
|
29 ex4 {A}{B} = A → B → B
|
|
|
30
|
|
|
31 ex5 : {A B : Set} → Set
|
|
|
32 ex5 {A}{B} = A → B → A
|
|
|
33
|
|
|
34 proof5 : {A B : Set } → ex5 {A} {B}
|
|
|
35 proof5 = {!!}
|
|
|
36
|
|
|
37
|
|
|
38 postulate S : Set
|
|
|
39 postulate s : S
|
|
|
40
|
|
|
41 ex6 : {A : Set} → A → S
|
|
|
42 ex6 a = {!!}
|
|
|
43
|
|
|
44 ex7 : {A : Set} → A → T
|
|
|
45 ex7 a = {!!}
|
|
|
46
|
|
|
47 ex11 : (A B : Set) → ( A → B ) → A → B
|
|
|
48 ex11 = {!!}
|
|
|
49
|
|
|
50 ex12 : (A B : Set) → ( A → B ) → A → B
|
|
|
51 ex12 = {!!}
|
|
|
52
|
|
|
53 ex13 : {A B : Set} → ( A → B ) → A → B
|
|
|
54 ex13 {A} {B} = {!!}
|
|
|
55
|
|
|
56 ex14 : {A B : Set} → ( A → B ) → A → B
|
|
|
57 ex14 x = {!!}
|
|
|
58
|
|
|
59 proof5' : {A B : Set} → ex5 {A} {B}
|
|
|
60 proof5' = {!!}
|
|
|
61
|
