--- a/a02/agda/lambda.agda	Wed Dec 18 17:34:15 2019 +0900
+++ b/a02/agda/lambda.agda	Sat Mar 14 17:34:54 2020 +0900
@@ -7,6 +7,11 @@
 lemma2 : (A : Set ) →  A → A 
 lemma2 A a = {!!}
 
+→intro : {A B : Set } → A →  B → ( A → B )
+→intro _ b = λ x → b
+
+→elim : {A B : Set } → A → ( A → B ) → B
+→elim a f = f a 
 
 ex1 : {A B : Set} → Set 
 ex1 {A} {B} = ( A → B ) → A → B