<p dir="ltr">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.</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, "Andreas Abel" <<a href="mailto:abela@chalmers.se">abela@chalmers.se</a>> 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'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't understand how we can define in Agda a type of "Symmetric<br>
Binary Relation". 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 "Binary operation"<br>
-}<br>
BinaryOperation = Ω → Ω → Ω<br>
<br>
{-<br>
I can actually define an example of Binary operation.<br>
-}<br>
_⊙_ : BinaryOperation<br>
x ⊙ x' = 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 "Symmetric Binary Operation"? 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 <>< 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>