[Agda] How can we define a type of symmetric binary operations
in Agda ?
Sergey Kirgizov
sergey.kirgizov at u-bourgogne.fr
Mon May 4 11:37:02 CEST 2015
Thanks Andreas!
On Fri, May 01, 2015 at 09:06:50AM +0200, Andreas Abel 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/
More information about the Agda
mailing list