[Agda] Using Data.Sets

[J.Burton at brighton.ac.uk]

Hi, how do I use the Sets library? I want to work with sets of Chars
and other types, but if I try, e.g., fromList [ 1 ] 

(List ℕ) !=< .Relation.Binary.DecTotalOrder
when checking that the expression [ 1 ] has type
.Relation.Binary.DecTotalOrder

So do I need to define the order before I can make a <Set> of a
datatype? I got lost looking for the definition of DecTotalOrder...
If this isn't the way this module is intended to be used I suppose I
should cook my own following the example of examples/simple-lib/Lib/Eq
for polymorphism & equality...?

Thanks,

Jim