--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/a02/agda/lambda.agda	Wed Dec 18 17:34:15 2019 +0900
@@ -0,0 +1,56 @@
+module lambda ( T : Set) ( t : T ) where
+
+
+A→A : (A : Set ) → ( A → A )
+A→A = λ A → λ ( a : A ) → a
+
+lemma2 : (A : Set ) →  A → A 
+lemma2 A a = {!!}
+
+
+ex1 : {A B : Set} → Set 
+ex1 {A} {B} = ( A → B ) → A → B
+
+ex1' : {A B : Set} → Set 
+ex1' {A} {B} =  A → B  → A → B
+
+ex2 : {A : Set} → Set 
+ex2 {A}  =  A → ( A  → A )
+
+ex3 : {A B : Set} → Set 
+ex3 {A}{B}  =  A → B
+
+ex4 : {A B : Set} → Set 
+ex4 {A}{B}  =  A → B → B
+
+ex5 : {A B : Set} → Set 
+ex5 {A}{B}  =  A → B → A
+
+proof5 : {A B : Set } → ex5 {A} {B}
+proof5 = {!!}
+
+
+postulate S : Set
+postulate s : S
+
+ex6 : {A : Set} → A → S
+ex6 a = {!!}
+
+ex7 : {A : Set} → A → T
+ex7 a = {!!}
+
+ex11 : (A B : Set) → ( A → B ) → A → B
+ex11 = {!!}
+
+ex12 : (A B : Set) → ( A → B ) → A → B
+ex12 = {!!}
+
+ex13 : {A B : Set} → ( A → B ) → A → B
+ex13 {A} {B} = {!!}
+
+ex14 : {A B : Set} → ( A → B ) → A → B
+ex14 x = {!!}
+
+proof5' : {A B : Set} → ex5 {A} {B}
+proof5' = {!!}
+