集合とその上の同値関係を一緒にした構造を亜集合〈setoid〉といいます。亜集合を特別な圏（やせた亜群）とみなすことにより、亜集合に圏論的概念を適用できます。「2つの亜集合が同値（同型とは別な概念）であることは、商集合が同型であることと同じ」を示すことを目標に説明します。
圏の一般論では難しい概念である圏同型、圏同値、関手のあいだの自然同型などが、亜集合においては具体的でハッキリした概念となります。亜集合を調べることは、特殊な事例により圏の概念を学ぶことにもなります。$`
\newcommand{\cat}[1]{ \mathcal{#1} }
\newcommand{\mbf}[1]{ \mathbf{#1} }
\newcommand{\mrm}[1]{ \mathrm{#1} }
\newcommand{\o}[1]{ \overline{#1} }
%\newcommand{\u}[1]{ \underline{#1} }
\newcommand{\id}{ \mathrm{id} }
\newcommand{\In}{ \text{ in }}
%\newcommand{\On}{ \text{ on }}
\newcommand{\Iff}{ \Leftrightarrow }
\newcommand{\Imp}{ \Rightarrow }
\newcommand{\op}{ \mathrm{op}}
\newcommand{\hyp}{\text{－} }
\newcommand{\twoto}{\Rightarrow }
\newcommand{\EQV}{\mathrel{\overset{\sim}{\equiv}} }
`$
内容：
亜集合の圏
亜集合〈setoid〉とは、集合 $`S`$ とその上の同値関係 $`\sim`$ のペア $`(S, \sim)`$ です。亜集合自体を $`X`$ とするとき、次の形で記述することにします。
$`\quad X = (|X|, \sim_X)`$
$`|X|`$ が亜集合 $`X`$ の台集合〈underlying set〉で、$`\sim_X`$ が亜集合 $`X`$ の同値関係〈equivalence relation〉です。台集合を絶対値記号で書くのは、後で亜集合を特殊な圏とみなすので、圏の対象集合〈set of objects〉の記法と合わせたからです。
$`X, Y`$ が亜集合のとき、$`X`$ から $`Y`$ への（亜集合の）準同型射〈homomorphism〉とは、写像 $`f:|X| \to |Y| \In \mbf{Set}`$ で次の条件を満たすものです。
$`\text{For }x, y\in |X|\\
\quad x \sim_X y \Imp f(x) \sim_Y f(y)
`$
準同型射と準同型射の関数結合〈function composition〉がまた準同型射であること、恒等写像が準同型射であることはすぐ分かるので、亜集合達とそのあいだの準同型射達は圏を形成します。この圏を $`\mbf{Setoid}`$ と書きます。
2つの亜集合 $`X, Y`$ が同型〈isomorphic〉であるとは、次のような（亜集合の）準同型射 $`f, g`$ があることです。
$`\quad f: X \to Y \In \mbf{Setoid}\\
\quad g: Y \to X \In \mbf{Setoid}\\
\quad f; g = \id_X \In \mbf{Setoid}\\
\quad g; f = \id_Y \In \mbf{Setoid}
`$
後で、同型より弱い関係である同値〈equivalent〉を導入します。先に注意しておくと、亜集合の（台集合の）要素の同値と、亜集合の同値は別物です（同じ言葉を異なる概念にオーバーロードしています）。
ホムセットと内部ホム対象
$`X, Y \in |\mbf{Setoid}|`$ として、$`X, Y`$ に対するホムセットは通常通り $`\mbf{Setoid}(X, Y)`$ と書きます。ホムセットは単なる集合で、亜集合ではありません。
ホムセットを亜集合にするために、ホムセットの要素のあいだの同値関係を導入します。 これから定義する、ホムセット $`\mbf{Setoid}(X, Y)`$ の上の同値関係を $`\approx_{X, Y}`$ とします。
$`\text{For }f, g \in \mbf{Setoid}(X, Y)\\
\quad f \approx_{X, Y} g \;:\Iff \forall x\in |X|. f(x) \sim_Y g(x)
`$
$`\approx_{X, Y}`$ が同値関係であることは容易に分かるでしょう。
亜集合（単なる集合ではない）$`\o{\mbf{Setoid}}(X, Y)`$ を次のように定義します。
$`\quad \o{\mbf{Setoid}}(X, Y) := ( \mbf{Setoid}(X, Y), \approx_{X, Y})`$
別な言い方をすれば：
- $`|\o{\mbf{Setoid}}(X, Y)| := \mbf{Setoid}(X, Y)`$
- $`\sim_{ \o{\mbf{Setoid}}(X, Y) }\; := \;\approx_{X, Y}`$
$`\o{\mbf{Setoid}}(X, Y)`$ を、内部ホム対象〈internal hom object〉または指数対象〈exponential object〉と呼びます（デカルト圏における内部ホム対象を特に指数対象と呼ぶことが多い）。こうして定義した内部ホム対象では、内部ホム対象を特徴付ける次の同型が成立します。
$`\text{For }X, Y, Z \in |\mbf{Setoid}|\\
\quad \mbf{Setoid}(X\times Y, Z)\cong \mbf{Setoid}(Y, \o{\mbf{Setoid}}(X, Z) )\; \In \mbf{Set}
`$
$`X\times Y`$ は亜集合の直積です -- どう定義するかは容易に想像がつくでしょう。内部ホム対象 $`\o{\mbf{Setoid}}(X, Z)`$ は習慣により $`[X, Z]_{\mbf{Setoid}}`$ あるいは単に $`[X, Z]`$ と略記します。この略記を使うと、上の同型はスッキリ書けます。
$`\quad \mbf{Setoid}(X\times Y, Z)\cong \mbf{Setoid}(Y, [X, Z] )\; \In \mbf{Set}`$
圏としての亜集合
亜集合 $`X \in |\mbf{Setoid}|`$ は圏とみなせます。圏とみなした亜集合も同じ $`X`$ で表すとして：
- 対象の集合： $`\mrm{Obj}(X) := |X|`$
- 射の集合： $`\mrm{Mor}(X) := \{(x, y)\in |X|\times |X| \mid x \sim_X y\}`$
- 射の域： $`\mrm{dom}( (x, y)) := x`$
- 射の余域： $`\mrm{cod}( (x, y)) := y`$
- 射の結合： $`(x, y); (y, z) := (x, z)`$
- 恒等射： $`\id_x := (x, x)`$
圏とみなした亜集合はやせた圏〈thin category〉（「はじめての圏論 その第3歩：極端な圏達 // 射が少ないやせた圏」参照）になります。つまり、ホムセット $`X(x, y)`$ は空集合か単元集合です。$`X(x, y)`$ が単元集合であることと、$`x \sim_X y`$ であることは同じことです。
$`x\sim_X y \Imp y\sim_X x`$ であることから、圏（としての） $`X`$ の射はすべて可逆射です。射がすべて可逆射である圏は亜群〈groupoid〉と呼びます。よって、亜集合はやせた亜群〈thin groupoid〉になります。
亜集合の準同型射である写像 $`f:|X| \to |Y|`$ は、射の集合 $`\mrm{Mor}(X), \mrm{Mor}(Y)`$ にまで拡張できます。拡張した写像も同じ $`f`$ で表すと $`f:\mrm{Mor}(X) \to\mrm{Mor}(Y)`$ 。これらは、関手の対象パート〈object part〉と射パート〈morphism part〉となり、全体として関手を定義します。関手性〈functoriality〉は容易に示せるでしょう。
亜集合は圏であり（正確に言えば、亜集合は圏とみなせて）、準同型射は関手であることが分かりました。関手のあいだの自然変換を考えることができます。自然変換 $`\alpha`$ は次のように書けます。
$`\text{For }f, g : X \to Y \In \mbf{Cat}\\
\quad (\alpha :: f \twoto g) := (\alpha_x : f(x) \to g(x) \In Y)_{x\in X}
`$
上記定義の $`f(x) \to g(x)`$ は、$`f(x) \sim_Y g(x)`$ と同じことです。よって、$`(\alpha :: f \twoto g)`$ であることは次のように書けます。
$`\quad \forall x\in X. f(x) \sim_Y g(x)`$
これは $`f \approx_{X,Y} g`$ にほかなりません。つまり、$`f`$ から $`g`$ への自然変換 $`\alpha`$ があることは、内部ホム対象（である亜集合）のなかで $`f`$ と $`g`$ が（$`\approx_{X,Y}`$ に関して）同値であることです*1。内部ホム対象（である亜集合）は、関手圏であり、関手圏の射である自然変換は、準同型射のあいだの同値関係 $`\approx_{X, Y}`$ に対応します。
以上のことをまとめると：
| 亜集合 | 圏として解釈すると |
|---|---|
| 亜集合 | やせた亜群 |
| 要素のあいだの同値関係 | 対象のあいだの射 |
| 要素のあいだの等値〈イコール〉関係 | 対象の恒等射 |
| 亜集合の準同型射 | 関手 |
| 内部ホム対象（である亜集合） | 関手圏 |
| 準同型射のあいだの同値関係 | 自然変換 ＝ 関手圏の射 |
関手圏の射である自然変換が可逆であるとき、その自然変換は自然同型〈natural isomorphism〉と呼びます。亜集合（を圏とみなした圏）に関しては、すべての自然変換が自然同型〈可逆〉です。
亜集合の同値性
2つの亜集合が同値〈equivalent〉であることは、同型〈isomorphic〉であることとは違うことです。等値、同型、同値などは似てますが異なる概念で混乱しがちです。次は違う概念なので区別しましょう。
- 亜集合 $`X`$ の2つの要素 $`x,y\in |X|`$ の同値関係 $`x \sim_X y`$ （圏論的には、対象の同型）
- 2つの亜集合 $`X, Y`$ の同型関係 $`X \cong Y \In \mbf{Setoid}`$ （圏論的には、圏同型）
- 2つの準同型射 $`f, g:X \to Y\In \mbf{Setoid}`$ の同値関係 $`f \approx_{X, Y} g`$ （圏論的には、関手の自然同型）
- これから定義する、2つの亜集合 $`X, Y`$ の同値関係 $`X \EQV Y \In \mbf{Setoid}`$ （圏論的には、圏同値）
では、2つの亜集合 $`X, Y`$ が同値（同型とは違う）であることを定義しましょう。同値の記号は '$`\EQV`$' を使います。繰り返しますが、$`\EQV`$ は $`\sim_X`$ とは別物です。
$`\text{For }X, Y \in |\mbf{Setoid}|\\
\quad X \EQV Y :\Iff \\
\qquad \exists f:X \to Y, g:Y \to X \In \mbf{Setoid}.\, f;g \approx_{X, X} \id_X \land g;f \approx_{Y, Y} \id_Y
`$
亜集合 $`X, Y`$ が同値であることは、圏とみなした $`X, Y`$ が圏同値〈equivalent categories〉であることと同じです。同値の定義に出てきた準同型射（関手に相当）$`f, g`$ または片一方のことも同値〈equivalence〉と呼ぶことが多いのですが、混乱をまねくので次の言い回しを使います。
- $`X \EQV Y`$ ： $`X`$ と $`Y`$ は同値〈equivalent〉である。
- $`f, g`$ ： $`f, g`$ は同値準同型射ペア〈equivalence homomorphism pair〉である。
- $`f`$ （または $`g`$） ： $`f`$ は同値準同型射〈equivalence homomorphism〉である。
$`f`$ が同値準同型射なら、$`f, g`$ が同値準同型射ペアとなる相方 $`g`$ が存在します。2つの亜集合のあいだに同値準同型射ペアが存在するなら、それらの亜集合は同値です。
圏論の一般的定理から、同値準同型射は、関手としてみなして充満忠実〈fully faithful〉で本質的に全射的〈essentially surjective〉です。ここでは、一般論ではなくて、亜集合に限定して同値準同型射の特徴付けを行います。亜集合の準同型射に関して忠実性〈faithfulness〉は自動的に満たされるので意味を持ちません。準同型射が充満で本質的に全射的〈full and essentially surjective〉であることを定義します。
亜群の準同型射が充満〈fulll〉であるとは次のことです。
$`\text{For }f: X \to Y \In \mbf{Setoid}\\
\quad f \text{ は充満} \;:\Iff \forall x, y\in X.\, f(x)\sim_Y f(y) \Imp x \sim_X y
`$
写像の値の側で同値なら、引数の側の同値性が言える、ということです。
亜群の準同型射が本質的に全射{的}?〈essentially surjective〉であるとは次のことです。
$`\text{For }f: X \to Y \In \mbf{Setoid}\\
\quad f \text{ は本質的に全射\{的\}?} \;:\Iff \forall y\in Y. \exists x\in X.\, y \sim_Y f(x)
`$
準同型射の写像が全射ならもちろん本質的に全射です。全射でなくても、$`Y`$ 上の同値関係 $`\sim_Y`$ をたどって像集合を広げると $`Y`$ 全体になるときは本質的に全射です。
亜集合の圏において、次が成立します。
$`\text{For }f: X \to Y \In \mbf{Setoid}\\
\quad f \text{ は同値準同型射} \Iff f \text{ は充満かつ本質的に全射}
`$
次節でこの命題を示します。
同値準同型射の特徴付け
前節最後の命題を次の3つの命題に分けます。
- $`f \text{ は同値準同型射} \Imp f \text{ は充満}`$
- $`f \text{ は同値準同型射} \Imp f \text{ は本質的に全射}`$
- $`f \text{ は充満かつ本質的に全射} \Imp f \text{ は同値準同型射}`$
一番目の命題の証明
次を仮定します。
$`\text{For }x, y\in |X|\\
\quad f(x) \sim_Y f(y)
`$
前提から $`f`$ は同値準同型射なので、相方である $`g:Y \to X \In \mbf{Setoid}`$ が存在します。上記の仮定に $`g`$ を適用すると：
$`\quad g(f(x)) \sim_X g(f(y))`$
これは、$`g`$ が亜集合の準同型射だからです。
$`f, g`$ が同値準同型射ペアなので、次も成立します。
$`\quad g(f(x)) \sim_X x`$
$`\quad g(f(y)) \sim_X y`$
これらから、$`x \sim_X y`$ が出ます。つまり次が言えました。
$`\text{For }x, y\in |X|\\
\quad f(x) \sim_Y f(y) \Imp x \sim_X y
`$
これは、$`f`$ が充満であることです。（証明終わり）
二番目の命題の証明
同値準同型射 $`f`$ の相方（存在する）をまた $`g:Y \to X \In \mbf{Setoid}`$ とします。任意に $`y \in Y`$ を取ったとして、$`a := g(y)`$ と置きます。
$`y \sim_Y f(a)`$ が成立します。なぜなら、$`y \sim_Y f(g(y))`$ は、$`f, g`$ が同値準同型射ペアであることから言えるからです。この $`a \in |X|`$ を証拠として次の命題を主張できます。
$`\quad \exists x\in X.\, y \sim_Y f(x)`$
$`y \in Y`$ は任意に取ったので、次が言えます。
$`\quad \forall y\in Y.\exists x\in X.\, y \sim_Y f(x)`$
これは、$`f`$ が本質的に全射であることです。（証明終わり）
三番目の命題の証明
充満かつ本質的に全射な $`f:X \to Y \In \mbf{Setoid}`$ から、同値準同型射ペアの相方 $`g: Y \to X \In \mbf{Setoid}`$ を構成します。任意の $`y\in |Y|`$ に対する値 $`g(y)\in |X|`$ を決めて（第一段階）、$`g`$ が亜集合の準同型射になっていることを示し（第二段階）、さらに $`f`$ の相方になっていることを示せば（第三段階）よいわけです。
第一段階； 任意に $`y\in Y`$ を取ったとき、$`f`$ は本質的に全射なので、$`y \sim_X f(x)`$ となる $`x \in X`$ は存在します。その $`x`$ に対して $`x \sim_X a`$ となるような $`a`$ （$`a = x`$ でもかまいません）を選びます。$`y\in |Y|`$ に対する $`a\in |X|`$ の選び方は色々あるでしょうが、とにかく1つ選んで $`g(y) := a`$ と決めます。すべての $`y\in Y`$ に対してこの方法で $`g(y)`$ を決めれば、写像 $`g:|Y| \to |X| \In \mbf{Set}`$ は確定します。（構成終わり） ただし、そうやって決めた $`g`$ が亜集合の準同型射であるかどうか？ $`f`$ の相方になっているか？ はまだ分かりません。
第ニ段階； $`g`$ が亜集合の準同型射であることを示しましょう。$`y,t \in |Y|,\; y \sim_Y t`$ と仮定します。次の状況になっているとします。
- $`y \sim_Y f(x),\; x \sim_X a,\; g(y) = a`$
- $`t \sim_Y f(s),\; s \sim_X b,\; g(t) = b`$
次のような絵を描いておくとよいでしょう。波線は要素のあいだの同値関係です。
$`\quad \xymatrix{
x \ar@{|->}[r]^{f} \ar@{~}[d]
\ar@{.}@/_2.5pc/[ddd]
& f(x) \ar@{~}[d]
\\
a = g(y)
& y \ar@{|->}[l]_{g} \ar@{~}[d]
\\
b = g(t)
& t \ar@{|->}[l]_{g}
\\
s \ar@{|->}[r]^{f} \ar@{~}[u]
& f(s) \ar@{~}[u]
}`$
この図を見ると、$`f(x) \sim_Y f(s)`$ は分かります。$`f`$ は充満だったので、$`x \sim_X s`$ が言えます（図の点線部分）。$`g(y), x, s, g(t)`$ と同値関係をたどると、$`g(y) \sim_X g(t)`$ が言えます。
つまり、次の命題が成立します。
$`\quad y \sim_Y t \Imp g(y) \sim_X g(t)`$
$`y, t`$ は任意に選んでいるので：
$`\quad \forall y, t\in Y.\, y \sim_Y t \Imp g(y) \sim_X g(t)`$
これは、$`g`$ が亜集合の準同型射であることです。（証明終わり）
第三段階；
上の図を見ると、$`g(y) \sim_X x`$ は分かります。$`f`$ を適用すると $`f(g(y)) \sim_Y f(x)`$ 、$`f(x) \sim_Y y`$ を考慮すれば $`f(g(y)) \sim_Y y`$ が言えます。$`y`$ は任意に取れるので、次が成立します。
$`\quad \forall y\in Y.\, f(g(y)) \sim_Y y`$
同様にして次も成立することが分かります。
$`\quad \forall x\in X.\, g(f(x)) \sim_X x`$
これらは、$`f, g`$ が同値準同型射ペアであることです。つまり、$`f`$ は同値準同型射です。（証明終わり）
商集合
亜集合 $`X \in |\mbf{Setoid}|`$ に対して、その商集合〈quotient set〉を次のように書きます。
$`\quad Q(X) := |X|/\sim_X \;\in |\mbf{Set}|`$
亜集合の準同型射 $`f:X \to Y \In \mbf{Setoid}`$ に対しても、集合のあいだの写像 $`Q(f)`$ を定義しましょう。
$`\text{For }f: X\to Y \In \mbf{Setoid}\\
\quad Q(f) : Q(X) \to Q(Y) \In \mbf{Set}
`$
$`x\in |X|`$ に対して、$`x`$ が属する同値類を $`[x]\in Q(X)`$ と書きます。
$`\text{For }x\in |X|\\
\quad Q(f)([x]) := [f(x)] \; \in Q(Y)
`$
と定義します。しかし、別な $`x' \in |X|`$ に対しても同じ同値類が対応することを確認する必要があります。つまり、次が必要です。
$`\quad x \sim_X x' \Imp [f(x)] = [f(x')]`$
これは、$`x \sim_X x' \Imp f(x) \sim_Y f(x')`$ と同じことなので、$`f`$ が準同型射であることから出ます。したがって、$`Q(f)`$ の定義は大丈夫〈well-defined〉です。
以上に定義した $`Q(\hyp)`$ は、亜群の圏から集合圏への関手となります。（細部は確認してみてください。）
$`\quad Q : \mbf{Setoid} \to \mbf{Set} \In \mbf{CAT}`$
商集合への標準射影も定義しておきましょう（あっ、これも「射影」だ。「射影、入射、セクション、レトラクション」参照）。$`T`$ は、集合を自明な亜集合とみなす関手だとします。
$`\quad T: \mbf{Set}\to \mbf{Setoid} \In \mbf{CAT}\\
\quad \text{where }T(S) := (S, =_S)
`$
集合 $`S`$ 上の等値〈イコール〉関係 $`=_S`$ は同値関係なので、$`(S, =_S)`$ は亜集合になります。集合 $`S`$ と亜集合 $`(S, =_S)`$ を区別しないことが多いですが、ここでは区別します。
亜集合 $`X`$ から商集合 $`T(Q(X))`$ への標準射影〈canonical projection〉を次のように書きます。
$`\text{For }X \in |\mbf{Setoid}|\\
\quad \pi_X : X \to T(Q(X)) \In \mbf{Setoid}\\
\quad \text{where }\pi_X(x) := [x]\; \in |T(Q(X))|
`$
$`\pi_X `$ は、単なる写像ではなくて亜群の準同型射です。次が成立します。
$`\quad \forall x, y\in |X|.\, x \sim_X y \Imp \pi_X(x) =_S \pi_X(y)`$
亜集合の同値性と商集合の同型性
次の命題は、実用的にも役に立ちます。
$`\text{For }X, Y \in |\mbf{Setoid}|\\
\quad (X \EQV Y \In \mbf{Setoid}) \Iff (Q(X) \cong Q(Y) \In \mbf{Set})
`$
この命題を次の2つの命題に分けて示します。
- $`(X \EQV Y \In \mbf{Setoid}) \Imp (Q(X) \cong Q(Y) \In \mbf{Set})`$
- $`(Q(X) \cong Q(Y) \In \mbf{Set}) \Imp (X \EQV Y \In \mbf{Setoid})`$
一番目の命題の証明
亜集合の同値 $`X\EQV Y`$ を与える同値準同型射ペアを $`f, g`$ とします。これらに $`Q`$ を適用すると、次が得られます。
$`\quad Q(f) : Q(X) \to Q(Y)\\
\quad Q(g) : Q(Y) \to Q(X)
`$
$`Q(f), Q(g)`$ が $`Q(X) \cong Q(Y)`$ を与える（集合の）同型射ペアになることを示しましょう。そのためには次が必要です。
$`\quad Q(f); Q(g) = \id_{Q(X)}\\
\quad Q(g); Q(f) = \id_{Q(Y)}
`$
$`Q`$ の関手性から、次でも同じです。
$`\quad Q(f;g) = \id_{Q(X)}\\
\quad Q(g; f) = \id_{Q(Y)}
`$
実際に計算してみます。$`Q(X)`$ の要素（同値類）は $`[x]`$ の形で書くとします。
$`\quad Q(f;g)([x]) \\
= Q(g\circ f)([x]) \\
= [(g\circ f)(x)]\\
= [g(f(x))] \\
= [x]
`$
最後の部分は $`g(f(x)) \sim_X x`$ を使っています。同様に：
$`\quad Q(g;f)([y]) \\
= Q(f\circ g)([y]) \\
= [(f\circ g)(y)] \\
= [f(g(y))] \\
= [y]
`$
最後の部分は $`f(g(y)) \sim_Y y`$ を使っています。
これで、$`Q(f)`$ と $`Q(g)`$ が互いに逆であることがわかりました。つまり、$`Q(X)`$ と $`Q(Y)`$ は集合として同型です。（証明終わり）
ニ番目の命題の証明
$`Q(X) \cong Q(Y)`$ を与える（集合の）同型射ペアを $`\varphi, \psi`$ とします。
$`\quad \varphi : Q(X) \to Q(Y) \In \mbf{Set}\\
\quad \psi : Q(Y) \to Q(X) \In \mbf{Set}\\
\quad \text{where }\varphi; \psi = \id_{Q(X)} \land \psi ; \varphi = \id_{Q(Y)}
`$
前節の標準射影とは別な、集合圏内での標準射影を $`\rho_X, \rho_Y`$ とします。集合圏内での標準射影 $`\rho_X, \rho_Y`$ は全射なので、セクション（「射影、入射、セクション、レトラクション」参照）が存在します。セクションを $`s, t`$ とします。図にまとめると次のようです。
$`\quad \xymatrix{
|X| \ar[d]^{\rho_X}
&|Y| \ar[d]_{\rho_Y}
\\
Q(X) \ar@/^1pc/[u]^{s} \ar@/^1pc/[r]^{\varphi}
& Q(Y) \ar@/_1pc/[u]_{t} \ar@/^1pc/[l]^{\psi}
}\\
\quad \text{where}\\
\qquad \varphi ; \psi = \id_{Q(X)}\\
\qquad \psi ; \varphi = \id_{Q(Y)}\\
\qquad s ; \rho_X = \id_{Q(X)}\\
\qquad t ; \rho_Y = \id_{Q(Y)}\\
\quad \In \mbf{Set}
`$
以上のセットアップで、台集合のあいだの写像 $`f, g`$ を定義し（第一段階）、$`f, g`$ が亜集合の準同型射になっていることを示し（第二段階）、$`f, g`$ が同値準同型射ペアになっていることを示せば（第三段階）よいわけです。
第一段階；
台集合のあいだの写像 $`f, g`$ を次のように定義します
$`\quad f:|X| \to |Y| \In \mbf{Set}\\
\quad \text{where }f := \rho_X ; \varphi ; t\\
\quad g:|Y| \to |X| \In \mbf{Set}\\
\quad \text{where }g := \rho_Y ; \psi ; s
`$
この定義で $`f, g`$ は確定します。（構成終わり）
第ニ段階；
次を示します。
$`\text{For }x, x'\in |X|\\
\quad x \sim_X x' \Imp f(x) \sim_Y f(x')
`$
定義に基づいて書き下すと：
$`f(x)= t(\varphi([x]))\\
f(x')= t(\varphi([x']))
`$
$`x \sim_X x'`$ ならば $`[x]= [x']`$ なので、$`f(x) = f(x')`$ 、イコールなら同値なので $`f(x) \sim_Y f(x')`$ は成立します。
同様に、次も言えます。
$`\text{For }y, y'\in |Y|\\
\quad y \sim_Y y' \Imp g(y) \sim_X g(y')
`$
$`f, g`$ は亜集合の準同型射になっています。（証明終わり）
第三段階；
$`x\in |X|`$ に対して、$`g(f(x))`$ を計算してみます。
$`\quad g(f(x))
= s( \psi( [t(\varphi([x]))] ) )
`$
この値が $`x`$ と同値であることを示すには、$`\rho_X`$ を適用した値が等しくなればいいので、$`\rho_X`$ を適用します。
$`\quad \rho_X( s( \psi( [t(\varphi([x]))] ) ) )\\
= \psi( [ t(\varphi([x])) ] ) \\
= \psi( \rho_Y ( t(\varphi([x])) )) \\
= \psi( \varphi([x]) ) \\
= [x]
`$
これで、$`[ g(f(x)) ] = [x]`$ が示せました。つまり、$`g(f(x)) \sim_X x`$ です。$`x`$ は任意に選んでいるので次が成立します。
$`\quad \forall x\in |X|.\, g(f(x)) \sim_X x`$
同様に、次も成立します。
$`\quad \forall y\in |Y|.\, f(g(y)) \sim_Y y`$
これは、$`f, g`$ が同値準同型射ペアであることです。（証明終わり）
おわりに
「有限コレクション： 再配置の圏から」において、再配置の圏 $`\cat{R}`$ に対して有限コレクションの集合 $`\mrm{FinColl}_{\cat{R}}(X)`$ を定義しました。具体例で見ると、2つの再配置の圏 $`\cat{R}, \cat{S}`$ が圏同値のとき、集合圏上の自己関手 $`\mrm{FinColl}_{\cat{R}}`$ と $`\mrm{FinColl}_{\cat{S}}`$ は自然同型になるようです。
とりあえず前節で述べた亜集合と商集合に関する命題は使いそうなので、説明付きで示してみました。
*1:内部ホム対象の同値関係に関して同値であることは、圏論で言えば関手圏内で同型であることで、自然同型と言います。
