lawless signature に法則を付け足すときの記法

構文は：

law 2-ラベル :: 閉じた論理式

または

variable 変数の型宣言

law 2-ラベル :: 自由変数を含む論理式

法則の圏論的実体〈シング〉は2-射なので、法則名は2-ラベルとする。

事例：

signature LawlessMonoid within Set {
  sort U
  operation e: 1 → U
  operation m: U×U → U
}

法則を付け加える。

signature Monoid within Set {
  sort U
  operation e: 1 → U
  operation m: U×U → U

  law assoc :: ∀x, y, z∈U. m(m(x, y), z) = m(x, m(y, z))
  law lunit :: ∀x∈U. m(e, x) = x
  law runit :: ∀x∈U. m(x, e) = x
}

または

signature Monoid within Set {
  sort U
  operation e: 1 → U
  operation m: U×U → U

  variable x, y, z∈U

  law assoc :: m(m(x, y), z) = m(x, m(y, z))
  law lunit :: m(e, x) = x
  law runit :: m(x, e) = x
}