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 )

proof2 : {A : Set } → ex2 {A}
proof2 = {!!}

ex3 : {A B : Set} → A → B
ex3 a = {!!}

ex4 : {A B : Set} → A → B → B
ex4 {A}{B} a b  =   {!!}

ex5 : {A B : Set} → A → B → A
ex5 = {!!}



postulate
  Domain : Set
  Range : Set
  r : Range 

ex6 : Domain → Range
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 = {!!}