module derivationsagdacode1 where 

postulate A : Set


f : A -> A
f = \(a : A) -> a