指標は宣言文の集まりです。各宣言文は、順番〈位置番号〉でも名前でも一意識別できます。実用上は、(順番は覚えにくいので)名前が使われます。が、理論上は名前が邪魔になることがあるので、ときに、名前を削除する必要があります。
名前の削除方法の記述が意外に見つからないので、ここに記しておきます。事例で示します。$`\newcommand{\mrm}[1]{ \mathrm{#1} }
\newcommand{\mbf}[1]{\mathbf{#1}}
\newcommand{\In}{ \text{ in } }
\newcommand{\id}{\mathrm{id} }
\newcommand{\twoto}{\Rightarrow }
\newcommand{\T}[1]{\text{#1} }
`$
事例として半群を考えます。その指標は以下のとおり。
$`\T{signature }\T{Semigroup} \:\{\\
\quad \T{sort } U \In \mbf{Set}\\
\quad \T{operationt } m : U\times U \to U \In \mbf{Set}\\
\quad \T{equation }\mrm{assoc} ::
(m\times \id_U); m \twoto \alpha_{U,U,U} ; (\id_U \times m); m
\In \mbf{Set}\\
\}
`$
このなかで、$`\mrm{assoc}`$ は、等号を集合圏の2-射とみなして書いた等式的法則です。以下の可換図式とまったく同じことです。
$`\quad \xymatrix{
(U\times U)\times U \ar[r]^{\alpha_{U,U,U}}
\ar[d]_{m \times \id_U}
& U\times (U\times U)
\ar[d]^{\id_U \times m}
\\
U\times U \ar[d]_{m}
& U\times U \ar[d]^{m}
\\
U \ar@{=}[r]
& U
}\\
\quad \text{commutative }\In \mbf{Set}
`$
指標内に出てくる名前 $`U, m, \mrm{assoc}`$ を、適当な接頭辞(ここでは文字 'a')と位置番号から作った $`a1, a2, a3`$ に置き換えます。すると:
$`\T{signature }\T{Semigroup} \:\{\\
\quad \T{sort } a1 \In \mbf{Set}\\
\quad \T{operationt } a2 : a1\times a1 \to a1 \In \mbf{Set}\\
\quad \T{equation } a3 ::
(a2\times \id_{a1}); a2 \twoto \alpha_{a1,a1,a1} ; (\id_{a1} \times a2); a2
\In \mbf{Set}\\
\}
`$
宣言文先頭のキーワードは無くてもいいので省略します。名前も位置番号(出現の順番)からわかるので省略、ただし構文の都合で場所取りのアンダースコアを書いておきます。すると:
$`\T{signature }\T{Semigroup} \:\{\\
\quad \_ \In \mbf{Set}\\
\quad \_ : a1\times a1 \to a1 \In \mbf{Set}\\
\quad \_ ::
(a2\times \id_{a1}); a2 \twoto \alpha_{a1,a1,a1} ; (\id_{a1} \times a2); a2
\In \mbf{Set}\\
\}
`$
接頭辞 'a' は別になんでもよくて、特に意味はありません。つまり、名前ではなくて位置番号 $`1, 2, 3`$ が識別子になっています。これで、名前は削除できました。
名前の削除は、しばしば暗黙に(なにも言わずに)行われます。「あれっ、名前はどうした?」と思ったら、暗黙に削除されたのかも知れません。名前を削除すると、指標のあいだのリネーム同値〈アルファ同値〉が等値〈イコール〉に変わります。名前の削除は、リネーム同値の同値類を取ることと同じ効果があります。
なお、名前の削除のためには、指標の宣言文のあいだに全順序〈total order〉が必要です。順番がなくて名前だけで識別されている場合は、名前の削除ができません。