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

[Dr. ERDI Gergo]

On Tue, 5 May 2015, Conor McBride wrote:

> Here's an old exercise of mine. Given
>
> data Nat : Set where
> ze : Nat
> su : Nat -> Nat
>
> symIter : {X : Set} -> (Nat -> X) -> (X -> X) -> Nat -> Nat -> X
> symIter zen more ze          n  = zen n
> symIter zen more m          ze  = zen m
> symIter zen more (su m) (su n)  = more (symIter zen more m n)
>
> Then define max, min, addition and multiplication by instantiating zen and
> more appropriately.

OK, I've done this exercise now. Multiplication is the odd one out that 
was tricky to implement; I wonder if there's a more straightforward way 
than mine?

https://gist.github.com/gergoerdi/46ad83513fd9db65c286

Now the real question is, what is the general, (semi-)mechanizable 
way of going from (some description of) an argument type A to the 
definition of

symIter :: {X : Set} -> (A -> X) -> (X -> X) -> A -> A -> X

?