指標実例の相等
summary.icon 指標の実例同士の相等
signature.icon
code:sig
A = Sig a1 a2 a3 .. in C
B = Sig b1 b2 b3 .. in C
A == B
<=> a1 == b1 ∧ a2 == b2 .. in C
definition.icon$ \mathrm{Sig} の実例同士の相等
$ A = B \overset{\text{def}}{\Longleftrightarrow} (a_1 = b_1) ∧ (a_2 = b_2)\wedge \cdots
where
$ C : 相等の定義された圏
$ \mathrm{Sig} :$ C における指標
$ A= \left\lang\mathrm{ Sig }\colon a_1,a_2,a_3,\dots\right\rang
$ B= \left\lang\mathrm{ Sig }\colon b_1,b_2,b_3,\dots\right\rang
dragoon8192.iconただし、並んでいるのは任意のk-射