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 = {!!}

→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

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' = {!!}