Is there an Agda library defining a type of finite set-like collections of elements of any type? Fin seems to be just for sets of numbers. What about sets of another type (or even a newly defined type)?