--- a/a02/agda/lambda.agda	Sat Mar 14 19:42:27 2020 +0900
+++ b/a02/agda/lambda.agda	Sun Dec 27 13:26:44 2020 +0900
@@ -22,23 +22,26 @@
 ex2 : {A : Set} → Set 
 ex2 {A}  =  A → ( A  → A )
 
-ex3 : {A B : Set} → Set 
-ex3 {A}{B}  =  A → B
+proof2 : {A : Set } → ex2 {A}
+proof2 = {!!}
 
-ex4 : {A B : Set} → Set 
-ex4 {A}{B}  =  A → B → B
+ex3 : {A B : Set} → A → B
+ex3 a = {!!}
 
-ex5 : {A B : Set} → Set 
-ex5 {A}{B}  =  A → B → A
+ex4 : {A B : Set} → A → B → B
+ex4 {A}{B} a b  =   {!!}
 
-proof5 : {A B : Set } → ex5 {A} {B}
-proof5 = {!!}
+ex5 : {A B : Set} → A → B → A
+ex5 = {!!}
 
 
-postulate S : Set
-postulate s : S
 
-ex6 : {A : Set} → A → S
+postulate
+  Domain : Set
+  Range : Set
+  r : Range 
+
+ex6 : Domain → Range
 ex6 a = {!!}
 
 ex7 : {A : Set} → A → T
@@ -56,6 +59,4 @@
 ex14 : {A B : Set} → ( A → B ) → A → B
 ex14 x = {!!}
 
-proof5' : {A B : Set} → ex5 {A} {B}
-proof5' = {!!}