[Agda] Type inference question

[Robert Rothenberg]

On 02/07/08 14:19 Noam Zeilberger wrote:

>>  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

{a: Set} -> a -> a -> Bool

> 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.

It's gotten it to to be accepted without by removing the { a: Set } in the 
definition.

I need the types to be general (sets with equality) for the lemmas that I 
want to prove.