[Agda] Equality of arguments in Agda

[Robert Rothenberg]

In Haskell, I can use the class system to define a function that works on 
any type with equality, e.g.

   transpose :: (Eq a) => a -> a -> a -> a
   transpose x y z | z == x    = y
                   | z == y    = x
                   | otherwise = z

But I am unsure how to define such a function in Agda. As there is no class 
system, how do I specify it should be type with equality, and then use it in 
the function definition?

Or if my only choice is to use something like if_then_else, then where is it 
defined in the standard library?

Regards,
Rob