Comment peut-on définir un type d'opérations binaires symétriques dans Agda?

Question

Je ne comprends pas comment on peut définir dans Agda un type de "Relation Symétrique Binaire". Imaginez que j'ai quelque chose comme:

{- 
    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 

Comment on peut définir un type "Opération Binaire Symétrique"? Avoir ce type, nous serons en mesure de définir ⊙ comme

_⊙_ : SymmetricBinaryOperation 
x ⊙ y = A 

et la preuve que ⊙ est symétrique ne sera exigée.

Answer 1

Développant mon commentaire: il n'y aurait pas moyen de définir SymmetricBinaryOperation que vous voulez, même s'il y avait une procédure de décision pour le contrôle de symmetryness, car SymmetricBinaryOperation doit porter une preuve Symmetry sur l'opération définie. C'est à dire. l'opération doit se mentionner dans sa propre signature de type, ce qui est clairement une boucle. (D'où mon point sur les classes de type est insensé aussi).