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

[Dr. ÉRDI Gergő]

What about creating them such that they are symmetric by construction? If
we had quotient types, one could easily make an "unordered pair" type, and
make unary relations over that.

Are there any useful tricks to do something similar in Agda?
On May 1, 2015 3:07 PM, "Andreas Abel" <abela at chalmers.se> wrote:

> You can create a record with two fields, one is your binary operation, the
> other the proof of symmetry.
>
> record SymBinOp : Set where
>   field
>     _⊙_ : BinaryOperation
>     proof-of-symmetry : ∀ x y → x ⊙ y == y ⊙ x
>
> That's it!
>
> On 30.04.2015 17:35, Sergey Kirgizov wrote:
>
>> 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
>>
>> {-
>>    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
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
>>
>
> --
> Andreas Abel  <><      Du bist der geliebte Mensch.
>
> Department of Computer Science and Engineering
> Chalmers and Gothenburg University, Sweden
>
> andreas.abel at gu.se
> http://www2.tcs.ifi.lmu.de/~abel/
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20150505/90095d46/attachment.html