この記事は書きかけ、書き上がったら本編に投稿してここからは削除。
モノ達を1：1に置き換えることが置換です。モノが名前だとすれば、置換は名前達をリネームすることになります。項・式のなかに登場する名前達を系統的にリネームすることがアルファ変換です。$`\newcommand{\mrm}[1]{\mathrm{#1}}
\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\pipe}{\mid }
\newcommand{\ccol}[1]{\boldsymbol{#1} }
%\newcommand{\msf}[1]{\mathsf{#1}}
\newcommand{\twoto}{\Rightarrow }
\newcommand{\In}{\text{ in } }
%\newcommand{\Imp}{ \Rightarrow }
\newcommand{\Iff}{\Leftrightarrow }
\newcommand{\hyp}{\text{－} }
\newcommand{\op}{\mathrm{op} }
%\newcommand{\id}{\mathrm{id} }
%\newcommand{\pto}{ \supseteq\!\to }
\newcommand{\u}[1]{\underline{#1}}
\newcommand{\cpal}[1]{\mathfrak{#1} }
%\newcommand{\msc}[1]{\mathscr{#1}}
`$
内容：
置換の亜群
有限集合のあいだの同型射〈可逆写像 | 双射 | 全単射〉を置換〈permutation〉と呼ぶことにします。
$`\quad f \text{ が置換 }\Iff (f :X \to Y \In {\bf FinSet}) \;\land\; f \text{ は同型}`$
$`X = Y`$ の場合だけを置換と呼ぶことも多いですが、ここでは、$`X`$ と $`Y`$ が違う有限集合でもいいとします。
例えば、$`X = \{1, 2, 3\}, Y = \{a, b, c\}`$ で、$`f`$ が次のような対応であるとき、$`f`$ は置換です。
$`\quad 1 \mapsto c\\
\quad 2 \mapsto b\\
\quad 3 \mapsto a
`$
もちろん、$`f`$ の域と余域が同じでもかまいません。次は、$`X = Y = \{1, 2, 3\}`$ である置換の例です。
$`\quad 1 \mapsto 3\\
\quad 2 \mapsto 2\\
\quad 3 \mapsto 1
`$
特別な置換として、何もしない置換があります。例えば：
$`\quad 1 \mapsto 1\\
\quad 2 \mapsto 2\\
\quad 3 \mapsto 3
`$
すべての有限集合達を対象類（類〈class〉は大きな集合）として、置換を射とする圏を構成できます。この圏を $`{\bf Perm}`$ と書きます。圏 $`{\bf Perm}`$ のすべての射は可逆〈同型〉です。すべての射が可逆である圏を亜群〈groupoid〉と呼ぶので、$`{\bf Perm}`$ は亜群です。よって、$`{\bf Perm}`$ を置換の亜群〈groupoid of permutations〉と呼びます。
亜群 $`{\bf Perm}`$ は、有限集合の圏 $`{\bf FinSet}`$ の部分圏です。
$`\quad {\bf Perm} \subset {\bf FinSet} \In {\bf CAT}`$
$`{\bf CAT}`$ は必ずしも小さくない圏達の2-圏です（が、気にしなくもいいです）。
関数のプロファイル記述
関数のプロファイル（入力と出力の仕様）を次のように書くことにします。
$`\quad f: (a: {\bf N}, b: {\bf R}, c:{\bf R}) \to {\bf R}`$
これは単に仕様を書いた（宣言した）だけで、関数 $`f`$ を定義はしていません。定義は、例えば型付きラムダ計算の構文を使えば次のようになります。
$`\quad f := \lambda\, (a: {\bf N}, b: {\bf R}, c:{\bf R}).(\, (b + c)^a \; \in {\bf R}\,)`$
関数のプロファイルの記述では、仮引数名〈formal parameter name〉（今の例では $`a, b, c`$）は不要です。次のプロファイル宣言でも先と同じことです。
$`\quad f: ({\bf N}, {\bf R}, {\bf R}) \to {\bf R}`$
しかし、多くのプログラミング言語では仮引数名も付けます。また、型付きラムダ計算の構文では、仮引数名〈ラムダ変数名〉がないと関数の定義が書けません。
ここでは、「プロファイル宣言でも関数定義でも仮引数名を付けるがリネームしてもよい」というルールを採用します。先の仮引数名 $`a, b,c `$ はリネームしてもよいので、以下のようなプロファイル宣言と関数定義をしても（内容的には）同じことになります。
$`\quad f: (n: {\bf N}, x: {\bf R}, y:{\bf R}) \to {\bf R}\\
\quad f := \lambda\, (n: {\bf N}, x: {\bf R}, y:{\bf R}).(\, (x + y)^n \; \in {\bf R}\,)`$
リネーム
前節の仮引数名のリネームは、次のような置換 $`\sigma`$ です。
$`\quad \sigma: \{a, b, c\} \to \{x, y, n\} \In {\bf Perm}\\
\qquad a \mapsto n\\
\qquad b \mapsto x\\
\qquad c \mapsto y
`$
この置換〈リネーム〉 $`\sigma`$ により、最初の（$`a, b, c`$ を使った）定義を書き換えました。
$`\tau`$ を別な置換だとします。
$`\quad \tau: \{a, b, c\} \to \{x_1, x_2, x_3\} \In {\bf Perm}\\
\qquad a \mapsto x_3\\
\qquad b \mapsto x_1\\
\qquad c \mapsto x_2
`$
この置換〈リネーム〉 $`\tau`$ により書き換えて、関数のプロファイル宣言と定義を書いてみると以下のようです。
$`\quad f: (x_3: {\bf N}, x_1: {\bf R}, x_2:{\bf R}) \to {\bf R}\\
\quad f := \lambda\, (x_3: {\bf N}, x_1: {\bf R}, x_2:{\bf R}).(\, (x_1 + x_2)^{x_3} \; \in {\bf R}\,)`$
$`x_3`$ が仮引数リスト〈ラムダリスト〉の最初に出現するのが気持ち悪いかも知れません。が、気持ち悪いからといって何か悪いことが起きるわけでもないので、知ったこっちゃねーです。
置換〈リネーム〉は、関数プロファイルとラムダ抽象〈lambda abstraction〉に現れる仮引数リスト〈ラムダリスト〉やラムダ式に作用して、その形を変えます。我々の約束・習慣では、仮引数名のリネームで形が変わっても、内容は変わってないから同じモノとみなします。
型付き変数名の集合と型付け保存のリネーム
前節の「仮引数名をリネームしても同じモノ」をもう少し精密に考えるために準備をしましょう。
まず名前とは何でしょうか？ 名前が何であるかに定義はないし、定義する必要もありません。“名前の集合”は単なる（なんでもいい）集合であり、その集合の要素を“名前”と呼ぶだけのことです。
名前の集合（つまり、なんでもいいから集合）を $`X`$ とします。$`X`$ は無限集合でもなんとかなりますが、ここでは有限集合に限定しておきます。型無しラムダ計算なら集合 $`X`$ だけで十分ですが、型付きラムダ計算のときは、名前への型の割り当て〈型付け | typing〉 $`t:X \to \cat{T}`$ も一緒に考えます。ここで、$`\cat{T}`$ は型の集合です。型とは何であるか？ の詮索も今は不要です。特定された集合 $`\cat{T}`$ の要素を型と呼ぶだけです。
名前の集合 $`X`$ と型付け $`t:X \to \cat{T}`$ の組 $`(X, t)`$ が型付き変数名の集合〈set of typed variable names〉です。記号の乱用で次のように書きます。
$`\quad X = (X, t)`$
記号の乱用が嫌だという人は、$`X`$ が型付き変数名の集合だとして、次のように書けば正確です。
$`\quad X = (\u{X}, t_X)`$
正確な書き方では、$`\u{X}`$ が“型付き変数名の集合”の台〈underlying thing〉である“名前の集合”、$`t_X`$ が $`X`$ の型付けです。正確な書き方をしないとうまく記述できないこともあります。
名前が何であるかを定義しないので、変数名が何であるかも定義しません。「変数名とは変数に付けられる名前である」なんて言明はナンセンスです。変数名が指す対象物〈referent | denotation〉である“変数そのもの”なんて存在しないし、考える必要もないからです。強いて言えば、「変数名」と「変数」は同義語で、どちらも無定義（集合の要素なだけ）です。
$`X = (\u{X}, t_X), Y = (\u{Y}, t_Y)`$ が2つの型付き変数名の集合のとき、集合のあいだの置換 $`\sigma : \u{X} \to \u{Y}`$ が型付けを保存する〈preserve typing〉とは次のことです。
$`\quad \forall x\in \u{X}.\, t_Y(\sigma(x)) = t_X(x)`$
集合の要素を名前と呼んでいたので、型付けを保存する置換は型付けを保存するリネーム〈typing-preserving rename〉と呼んでもいいでしょう。
型の集合を $`\cat{T}`$ として、型付き変数名の集合を対象として、型付けを保存する置換を射とする亜群が構成できます。その亜群を $`\cat{T}\text{-}{\bf TypedPerm}`$ とします。単元集合を $`{\bf 1}`$ としたときに、次が成立します。
$`\quad {\bf 1}\text{-}{\bf TypedPerm} \cong {\bf Perm} \In {\bf GRPD}`$
ここで、$`\cong`$ は圏同型（圏同値より強い）を表し、$`{\bf GRPD}`$ は必ずしも小さくない亜群達の2-圏です。が、圏論的な背景はあまり気にする必要はなくて、「型が1つだけの『型付き』は『型無し』と同じこと」という主張を理解してください。
