Agda类型检查器拒绝半群简单定义的问题求助

核心错误 #

你定义的半群结合律assoc类型完全错误：

• 半群的结合律是等式关系，应该用Agda的命题等价类型_≡_来表达，而非函数类型A → B。
• 函数类型A → B要求左侧的A是一个Sort（比如Set、Set₁这类类型的类型），但你的(x ◇ y) ◇ z是X类型的项，X是Set而非Sort，所以触发了"X should be a sort, but it isn't"的错误。

额外问题 #

你在结构中加入了单位元e，这其实是**幺半群（Monoid）**的特征，半群（Semigroup）只需要满足结合律的二元运算，不需要单位元。

修正后的代码 #

正确的半群定义 #

首先导入命题等价类型：

open import Relation.Binary.PropositionalEquality

然后定义半群：

record Semigroup : Set₁ where
  field
    X : Set
    _◇_ : X → X → X
    assoc : ∀ {x y z} → (x ◇ y) ◇ z ≡ x ◇ (y ◇ z)

如果实际需要定义幺半群（带单位元） #

record Monoid : Set₁ where
  field
    X : Set
    e : X
    _◇_ : X → X → X
    assoc : ∀ {x y z} → (x ◇ y) ◇ z ≡ x ◇ (y ◇ z)
    identityˡ : ∀ x → e ◇ x ≡ x  -- 左单位元定律
    identityʳ : ∀ x → x ◇ e ≡ x  -- 右单位元定律

内容的提问来源于stack exchange，提问作者user1023733