[Agda] Type inference question

[Robert Rothenberg]

> transpose : {a : Code} -> El a -> El a -> El a -> El a
> transpose x y z =
>   if z == x then y
>   else if z == y then x
>   else z

Instead of passing three arguments to transpose, I would like to combine the 
first two into a pair, and define a dot operator for applying a 
transposition to an individual:

  data Transposition (a : Set) : Set where
   ≪_,_≫ : a -> a -> Transposition a

  _·_ : { a : Set } -> Transposition a -> a -> a
  ≪ x , y ≫ · z = if (z == x) then y
                 else if (z == y) then x
                 else z

but this doesn't work. I get an error

  .a != a of type Set
  when checking that the expression z has type a

It seems clear to me that z is of type a, but not to Agda.  What do I need 
to do to fix this?

Rob