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

[Andreas Abel]

Looks like you want a higher inductive type...

On 05.05.2015 08:27, Dr. ÉRDI Gergő wrote:
> 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
> <mailto: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 <mailto: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 <mailto:andreas.abel at gu.se>
>     http://www2.tcs.ifi.lmu.de/~abel/
>     _______________________________________________
>     Agda mailing list
>     Agda at lists.chalmers.se <mailto: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/