|
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
|
|
|
10
|
|
|
11 ex1 : {A B : Set} → Set
|
|
|
12 ex1 {A} {B} = ( A → B ) → A → B
|
|
|
13
|
|
|
14 ex1' : {A B : Set} → Set
|
|
|
15 ex1' {A} {B} = A → B → A → B
|
|
|
16
|
|
|
17 ex2 : {A : Set} → Set
|
|
|
18 ex2 {A} = A → ( A → A )
|
|
|
19
|
|
|
20 ex3 : {A B : Set} → Set
|
|
|
21 ex3 {A}{B} = A → B
|
|
|
22
|
|
|
23 ex4 : {A B : Set} → Set
|
|
|
24 ex4 {A}{B} = A → B → B
|
|
|
25
|
|
|
26 ex5 : {A B : Set} → Set
|
|
|
27 ex5 {A}{B} = A → B → A
|
|
|
28
|
|
|
29 proof5 : {A B : Set } → ex5 {A} {B}
|
|
|
30 proof5 = {!!}
|
|
|
31
|
|
|
32
|
|
|
33 postulate S : Set
|
|
|
34 postulate s : S
|
|
|
35
|
|
|
36 ex6 : {A : Set} → A → S
|
|
|
37 ex6 a = {!!}
|
|
|
38
|
|
|
39 ex7 : {A : Set} → A → T
|
|
|
40 ex7 a = {!!}
|
|
|
41
|
|
|
42 ex11 : (A B : Set) → ( A → B ) → A → B
|
|
|
43 ex11 = {!!}
|
|
|
44
|
|
|
45 ex12 : (A B : Set) → ( A → B ) → A → B
|
|
|
46 ex12 = {!!}
|
|
|
47
|
|
|
48 ex13 : {A B : Set} → ( A → B ) → A → B
|
|
|
49 ex13 {A} {B} = {!!}
|
|
|
50
|
|
|
51 ex14 : {A B : Set} → ( A → B ) → A → B
|
|
|
52 ex14 x = {!!}
|
|
|
53
|
|
|
54 proof5' : {A B : Set} → ex5 {A} {B}
|
|
|
55 proof5' = {!!}
|
|
|
56
|
