<p dir="ltr">What about creating them such that they are symmetric by construction? If we had quotient types, one could easily make an &quot;unordered pair&quot; type, and make unary relations over that.</p>
<p dir="ltr">Are there any useful tricks to do something similar in Agda?</p>
<div class="gmail_quote">On May 1, 2015 3:07 PM, &quot;Andreas Abel&quot; &lt;<a href="mailto:abela@chalmers.se">abela@chalmers.se</a>&gt; wrote:<br type="attribution"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">You can create a record with two fields, one is your binary operation, the other the proof of symmetry.<br>
<br>
record SymBinOp : Set where<br>
  field<br>
    _⊙_ : BinaryOperation<br>
    proof-of-symmetry : ∀ x y → x ⊙ y == y ⊙ x<br>
<br>
That&#39;s it!<br>
<br>
On 30.04.2015 17:35, Sergey Kirgizov wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Hello,<br>
        <br>
I don&#39;t  understand how  we can  define in Agda  a type  of &quot;Symmetric<br>
Binary Relation&quot;. Can you help me?<br>
Imagine I have something like:<br>
<br>
=======================================================<br>
<br>
{-<br>
   At first we reaname  Set<br>
<br>
{-<br>
   First, we define a polymorphic idenity<br>
-}<br>
data _==_ {A : 𝓤} (a : A) : A → 𝓤 where<br>
   definition-of-idenity : a == a<br>
infix 30 _==_<br>
<br>
{-<br>
  Next we define the finite set Ω = {A,B,C}<br>
-}<br>
data Ω : 𝓤 where<br>
   A B C : Ω<br>
<br>
{-<br>
  We add a type &quot;Binary operation&quot;<br>
-}<br>
BinaryOperation = Ω → Ω → Ω<br>
<br>
{-<br>
  I can actually define an example of Binary operation.<br>
-}<br>
_⊙_ : BinaryOperation<br>
x ⊙ x&#39; = A<br>
infix 40 _⊙_<br>
<br>
{-<br>
  And then I can proove that ⊙ is Symmetric<br>
-}<br>
proof-of-symmetry : ∀ x y → x ⊙ y == y ⊙ x<br>
proof-of-symmetry = λ x y → definition-of-idenity<br>
<br>
<br>
========================================================<br>
<br>
How we  can define a  type &quot;Symmetric Binary Operation&quot;?   Having this<br>
type we will be able to define ⊙ as<br>
<br>
_⊙_ : SymmetricBinaryOperation<br>
x ⊙ y = A<br>
<br>
and proof that ⊙ is symmetric will no be required.<br>
<br>
<br>
Best regards,<br>
Sergey<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
<br>
</blockquote>
<br>
<br>
-- <br>
Andreas Abel  &lt;&gt;&lt;      Du bist der geliebte Mensch.<br>
<br>
Department of Computer Science and Engineering<br>
Chalmers and Gothenburg University, Sweden<br>
<br>
<a href="mailto:andreas.abel@gu.se" target="_blank">andreas.abel@gu.se</a><br>
<a href="http://www2.tcs.ifi.lmu.de/~abel/" target="_blank">http://www2.tcs.ifi.lmu.de/~abel/</a><br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>