[Agda] Type inference question

[Noam Zeilberger]

On Wed, Jul 02, 2008 at 01:19:14PM +0100, Robert Rothenberg wrote:
> >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

What is the type of the _==_ function?  In the body of transpose, it's
used at type {a : Code} -> El a -> El a -> Bool, but in the body of
_·_ it's apparently used at type {a : Set} -> a -> a -> Bool.  Try
making the types of Transposition and _·_ less general.

Noam