等価性 (Equality)

~ は2つのセルの間の 等価性 を表す型です。

基本

u: *
x: u → u
y: u → u
e: x ~ y

e は x と y が等しいことを示す 2-cell です。→ と同じく arrow 型ですが、方向を持たない（対称的な）関係を表現します。

`→` との違い

型	意味	方向
`x → y`	`x` から `y` への射	あり
`x ~ y`	`x` と `y` の等価性	なし

→ は一方向の射を表しますが、~ は双方向の等価関係を表します。

定義 (`:=`) との関連

定義 (:=) を使うと、等価性が自動的に生成されます。

x: * := y

これは x: * を宣言し、x.def: x ~ y を自動生成します。x と y は異なるセルとして存在しますが、評価上は等しいことを ~ で表現しています。