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

[Sergey Kirgizov]

also  I found Cody's post[1] about

"refinement types [that] capture the notion of contracts, and are also
related to axiomatic semantics or Hoare logic"

It's exaclty what I'm spekaing  about. But, if I understood correctly,
there is  no refinement types in  current Agda.  I'm also  afraid that
refinement  types  are not  entirely  compatible  with dependent  type
approach.

--
[1] http://cstheory.stackexchange.com/questions/16953/constraint-types-ibm-x10-compared-to-dependent-types/16975#16975

On Tue, May 05, 2015 at 11:27:17AM +0200, Andreas Abel wrote:
> 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/