types - 我们如何在 Agda 中定义一种对称二元运算？

Question

我不明白我们如何在 Agda 中定义一种“对称二元关系”。想象一下我有这样的东西:

{-
  First, we define a polymorphic idenity
-}
data _==_ {A : Set} (a : A) : A → Set where
  definition-of-idenity : a == a
infix 30 _==_

{-
 Next we define the finite set Ω = {A,B,C}
-}
data Ω : Set 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

我们如何定义“对称二元运算”类型？有了这个类型，我们就可以将⊙定义为

_⊙_ : SymmetricBinaryOperation
x ⊙ y = A

无需证明⊙是对称的。

Answer 1

阐述我的评论:没有办法按照你的意愿定义 SymmetricBinaryOperation，即使有一个检查对称性的决策程序，因为 SymmetricBinaryOperation 必须携带一个 Symmetry 关于被定义操作的证明。 IE。该操作必须在自己的类型签名中提及自己，这显然是一个循环。 (因此我关于类型类的观点也是毫无意义的)。