[Agda] How can we define a type of symmetric binary operations in Agda ?

[Matteo Acerbi]

On Wed, May 6, 2015 at 10:21 AM, Conor McBride
<conor at strictlypositive.org> wrote:
>
> On 5 May 2015, at 16:08, Sergey Kirgizov <sergey.kirgizov at u-bourgogne.fr> wrote:
>
> [..]
>
>> Indeed  "symIter"  is  a  beautiful  solution  for  defining  symetric
>> operations over finite  and denumerable sets.
>>
>> Do I understand correctly that it will work only with finite and denumerable sets?

It can be generalised to work on a class of datatypes which contains sets
that are neither finite nor denumerable:

https://gist.github.com/ma82/d76f51aa48ceee5a8766

Best,
Matteo

PS. I am not suggesting to use that encoding in practice. :-)