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

[Sergey Kirgizov]

Hello,
	
I don't  understand how  we can  define in Agda  a type  of "Symmetric
Binary Relation". Can you help me?
Imagine I have something like:

=======================================================

{-
  At first we reaname  Set to 𝓤 (as in Universe)
-}
𝓤 = Set

{-
  First, we define a polymorphic idenity
-}
data _==_ {A : 𝓤} (a : A) : A → 𝓤 where
  definition-of-idenity : a == a
infix 30 _==_

{-
 Next we define the finite set Ω = {A,B,C}
-}
data Ω : 𝓤 where
  A B C : Ω

{-
 We add a type "Binary operation"
-}
BinaryOperation = Ω → Ω → Ω

{-
 I can actually define an example of Binary operation.
-}
_⊙_ : BinaryOperation
x ⊙ x' = A
infix 40 _⊙_

{-
 And then I can proove that ⊙ is Symmetric
-}
proof-of-symmetry : ∀ x y → x ⊙ y == y ⊙ x
proof-of-symmetry = λ x y → definition-of-idenity


========================================================

How we  can define a  type "Symmetric Binary Operation"?   Having this
type we will be able to define ⊙ as

_⊙_ : SymmetricBinaryOperation
x ⊙ y = A

and proof that ⊙ is symmetric will no be required.


Best regards,
Sergey