プログラミング/圏論入門 の履歴(No.6)

目次†

有向グラフ†

圏をイメージするには「対象」同士を結ぶ「矢印」を描くと分かりやすい。

この図では黒丸が「対象」、矢印が「射」を表す。
いわゆる「有向グラフ」になっている。

ここには $O=\set{A,B,C}$ で３つの「対象」が存在する。

また、例えば $\mathrm{hom}(A,B)=\set{d, e}$ が $A$ から $B$ へ向かう矢印の集合であるとする。

• $\mathrm{hom}(A,A)=\set{a}$
• $\mathrm{hom}(B,B)=\set{b}$
• $\mathrm{hom}(C,C)=\set{c}$
• $\mathrm{hom}(A,B)=\set{d, e}$
• $\mathrm{hom}(B,A)=\set{}$
• $\mathrm{hom}(B,C)=\set{f}$
• $\mathrm{hom}(C,B)=\set{}$
• $\mathrm{hom}(A,C)=\set{g,h}$
• $\mathrm{hom}(C,A)=\set{}$

である。

射が向きを持つこと、ある対象から同じ対象へ戻る射 (例：$a,b,c$) が許されること、に注意せよ。

射の実態と $\mathrm{hom}$ の向き†

同じ図を $\mathrm{hom}(\cdot,\cdot)$ の中身を入れ替えて、$\mathrm{hom}'(B, A)=\set{d, e}$ のように、$B,A$ の順で $A$ から $B$ への矢印の集合を表すと定義しなおして新たな圏を構成しても構わない。$\mathrm{hom}(\cdot,\cdot)$ に与える対象の順番が、射の何の方向を決めるか(矢印の方向か、その逆方向か、など)は $\mathrm{hom}(\cdot,\cdot)$ の定義次第である。

Set 圏 = すべての集合とすべての写像が作る圏†

で、始めて圏論を学ぶ際には、「射」の実態として「写像」を思い浮かべると理解しやすい。

写像 $f:A\to B$ は任意の $x\in A$ に対して $f(x)\in B$ となる値を計算する規則（関数）であった。このとき$A$は始域、$B$は終域と呼ばれる。上で射とされた $a,b,c,\dots,h$ がそれぞれ個別の写像であり、$A,B,C$ はそれらの始域や終域となるクラス（集合）であると考える。これは実際、かなりメジャーな圏の構成である。

特に、$O$ をすべての集合を集めたクラスとし（これは真のクラスになる）、$\mathrm{hom}$ を２つの集合の間に考え得るすべての可能な写像の集合（こちらは集合になる）とする圏には Set 圏という名前がついている。

射の満たすべき公理†

圏論は個々の写像が始域の個々の要素を終域のどの要素へ移すか、という個別事情に立ち入らないまま、写像同士の合成について論じる手法を与える。

そのために圏論で射に要求される公理を、写像の言葉で理解すると次のようになる：

1. 射（写像）は常に合成可能である
   　　→ $f:A\to B,\ g:B\to C$ があるならそれを合成した $g\circ f: A\to C$ も必ず圏に含まれる
   
   
2. 合成に結合則が成り立つ
   　　→ 任意の $f:A\to B,\ g:B\to C,\ h:C\to D$ に対して
   　　$(h\circ g)\circ f=h\circ (g\circ f)$ が常に成り立つ
   
   
3. 任意の対象が恒等射（恒等写像）$1$ を持つ
   　　→ 各対象ごとに、任意の $f:A\to B$ に対して、$f=f\circ 1_A=1_B\circ f$
   　　を満たす写像 $1_A:A\to A,\ 1_B:B\to B$ が必ず存在する（恒等射の定義も兼ねている）

したがって、上の図の系が圏であるためには、

• $a=1_A$
• $b=1_B$
• $c=1_C$
• $g=f\circ d$
• $h=f\circ e$

であることが要求される（$g,h$ は逆でもいい）。

このように一般の有向グラフは「合成に対して閉じていること」や「恒等写像が存在すること」を満たさないため、そのままでは圏にはならない。この２つの要請は圏の性質を強く縛るものになっている。

対象の内部構造に踏み込まず、射の性質のみで公理化する†

恒等射が「要素を変更しない」のような要素レベルの言葉ではなく、
「別の射と合成したときに変化させない」のように射レベルの言葉で定義されていることに注意せよ。

このように圏論では対象の内部構造に踏み込まず、射の性質のみで公理化する手法が用いられ、
これをしばしば「普遍的な議論の方法」と呼ぶ。

これは、対象を外から見て射のレベルで同じなら、対象の内部構造に寄らず普遍的に適用可能な議論の方法、というような意味だ。

圏論における恒等射は要素を変え得る†

そして、要素レベルの定義と、射レベルの定義とが
決定的に異なる結果を生む場合があることにも注意が必要だ。

最も顕著な例として、ある対象 $A$ へ出入りする射が恒等射 $e$ しかない場合を考える。
このとき上の３つの公理は実質的に「恒等射が冪等であること $e\circ e=e$」しか求めない。

1. $e\circ e=e$ であれば閉じている
2. $(e\circ e)\circ e=e\circ (e\circ e)=e$ は結合則を満たす
3. 任意の $f:A\to B$ や $g:B\to A$ というのが $e$ しかないので恒等性も $e\circ e=e$ しか要求しない

恒等射に「要素を変えない」という要請が与えられないのだ。

例えば 「ゼロを掛ける」 や 「何らかの射影」 のような写像は冪等だ。
つまり実際にはそのような「要素を変化させる射」が「恒等射」とみなされうるのである。

他の射との合成で「本当は恒等でない」という事実が「ばれない」限り、それは恒等と見なされる。

射の合成のみで議論を進める圏論ではこう言うケースがそこここに出てくることに注意せよ。

恒等写像は対象あたり高々１つしか存在しない†

それでも上記の射レベルの公理のみで様々な有用な定理や概念を導けることを以下に見る。

１つ簡単な例をここで挙げれば、
ある対象 $A$ の上の恒等写像は高々１つだけであることを次のように示せる。

$1_A:A\to A,1'_A:A\to A$ がどちらも $A$ の恒等写像であるとすると、
$1_A=1_A\circ 1'_A=1'_A$ となって両者は等しい。

定理：同型な対象は、周囲の対象と必ず同じ本数の射で結ばれている†

$A,B$ が同型であるとすると、$f:A\to B$ と $f^{-1}:B\to A$ が存在する。

ある $C$ に対して、

• $g:C\to A$ が存在するなら、それに対応して $f\circ g:C\to B$ が必ず存在する
• $h:A\to C$ が存在するなら、それに対応して $h\circ f^{-1}:B\to C$ が必ず存在する

このように、同型であることと、射の合成が常に可能であること、の組み合わせにより、 同型な対象は圏の中にとてもよく似た構造を持つことになる。

プローブ対象、一般化された元、錐†

この $C$ のように興味範囲の対象に元を供給する源となる対象は「プローブ対象(probing object)」と呼ばれ、元を生成する射 $f,g,h$ 自体のことを「一般化された元(generalized element)」と呼ぶ。

個々の元そのものを考える代わりに、プローブ対象から各対象へ一般化された元が伸びる構造（「錐(cone)」と呼ばれる）で代用するのは圏論の標準的な手法である。

プローブ対象$C$を一般化された元$f$で移した像$f(C)$が、飛び先の対象の中で有効な元の範囲となることからも分かる通り、「圏全体に含まれるいずれの射からも生成されない元」は、圏論では「存在しないもの」とみなされる。これは全射・単射の議論でも出てきた話だった。

また、ここまでの話は対象が集合で、射がその間を結ぶ写像であるという前提での議論になっていたが、上記の積やプローブ対象、一般化された元、錐などの概念は、より一般的な圏では異なる意味を持つことになる。

余積構造を持つ写像 = 直和†

$\mathcal C$ での積が $\mathcal C^{\mathrm{op}}$ で余積に見える、というのはその通りであるが、それとは別に
$\mathcal C$ 内に余積構造を持つ写像を構成することも可能である。

$\alpha\in A,\beta\in B$ のとき、特殊な元 $\mathrm{null}$ を使って、
$D=A+B$ を $\set{(\alpha,\mathrm{null})}\cup\set{(\mathrm{null},\beta)}$ と定義し、
$p:\alpha\mapsto (\alpha,\mathrm{null})$
$q:\beta\mapsto (\mathrm{null},\beta)$
とする。

$h$ を、

• $A+B$ の元が $\alpha$ のみ含んでいるか、$\beta$ のみ含んでいるかを判別
• その結果をもとに適切に $f$ または $g$ を適用
• $f(\alpha)$ または $g(\beta)$ を返す

とすれば、$h\circ p=f,\ h\circ q=g$ が成り立つ。

$A,B$ の元をごちゃまぜに $A+B$ に突っ込んだところから、
それらを適切に分離して $A$ または $B$ の元を取り出す方法が一意に定まる、
というのが余積の構造であると読み取ることができる。

圏における積が対象の直積に相当するのに対して、
圏における余積は対象の直和に相当する。

同型関手†

関手 $\mathcal F:\mathcal C\to \mathcal C'$ が逆関手 $\mathcal F^{-1}:\mathcal C'\to \mathcal C$ を持つ、
すなわち $\mathcal F\circ \mathcal F^{-1}$ や $\mathcal F^{-1}\circ \mathcal F$ が恒等写像になるように $\mathcal F^{-1}$ を構成できるとき、
関手 $\mathcal F$ は同型関手であり、$\mathcal C$ と $\mathcal C'$ は同型である、と言う。

逆関手が存在する条件は、通常の写像と同様に関手$\mathcal F$が全単射であることと同値である。

関手$\mathcal F$の性質は対象の写像$\mathcal F_o$と射の写像$\mathcal F_m$とに分けて考えられるが、
このうち射の写像$\mathcal F_m$については特別に、

写像 $\mathcal F_m$ が $\mathrm{hom}(A,B)\to \mathrm{hom}'(\mathcal F_o(A),\mathcal F_o (B))$ の写像として

• 単射であることを 忠実
• 全射であることを 充満

というように 忠実 および 充満 の語が定義されている。
「充満忠実な関手」と言うのは $\mathcal F_m$ が全単射であることと同値である。

関手$\mathcal F$が全体として全単射であるためには充満忠実に加えて対象の写像 $\mathcal F_o$ が全単射である必要がある。

（関手$\mathcal F$が同型関手) = （関手$\mathcal F$が逆写像を持つ) =
(関手$\mathcal F$が全単射) = (充満忠実 = $\mathcal F_m$ が全単射) + ($\mathcal F_o$ が全単射)

同値関手†

注目する部分圏に同型な対象が複数存在するとき、圏の「同型」を少し緩めた「同値」という概念が役に立つことがある。

「同型な対象」とは両者の間に射と逆射のペアが定義された２つの対象のことであった。対象が集合であるなら、両者の要素の間に全単射による一対一対応がある状況を思い浮かべると良い。

部分圏が同型な対象を複数含むとき、関手がそのどれを、相手のどれに対応付けるか、には任意性がある。

例題として、$\mathcal C$ が含む $A,B,C$ が互いに同型な対象であるとしよう。
これらをそれぞれ $\mathcal C'$ が含む $A',B',C'$ に対応させて同型関手になるならそれらも同型であるから、

$A\mapsto A', B\mapsto B', C\mapsto C'$ と対応付ける代わりに、
$A\mapsto B', B\mapsto C', C\mapsto A'$ と対応付けても同型な関手を作ることが可能ということ。

それをさらに進めて、
$A\mapsto A', B\mapsto A', C\mapsto A'$ のようにつぶしてしまっても本質的な構造は保たれるから、
こういう「同型よりも少し緩い対応付けの取れる圏同士」を「同値」と呼ぼう、という話。

逆に、
$\mathcal C$ には $A$ しかないが、
$\mathcal C'$ は $A$ に対応する $A'$ と同型な $B',C'$ も含むとする。

このとき、
$\mathcal C$ から $\mathcal C'$ へ延びる関手は $A\mapsto A'$ だけで、$B',C'$ に対応付けるための対象が不足するが、このときも同型を代表して $A'$ に対応付けられていれば $\mathcal C$ と $\mathcal C'$ 全体 ($B',C'$ を含む) とが同値である、と呼ぶ。
（こう定義することで「同値」が対称律を持つようになる）

自己関手†

圏を自分自身の上へ移す関手のこと。

具体例：リスト関手†

例えば、プログラム上の型を対象として、関数を射とする圏において、型 $A,B$ と射 $f:A\to B$ があるとしよう。

リスト関手$\mathcal F$ は任意の型をその型を要素とするリストに変換し、任意の射をリストを受け取り、個々の要素に射を適用して結果のリストを返す射に変換する。

• $\mathcal F_o(A)=\mathrm{List}\langle A\rangle$
• $\mathcal F_o(B)=\mathrm{List}\langle B\rangle$
• $\mathcal F_m(f)=(\mathrm{list}: \mathrm{List}\langle A\rangle)=>\mathrm{list.map}(f)$
• $\mathcal F_m(1_A)=1_{\mathrm{List}\langle A\rangle}$
• $\mathcal F_m(1_B)=1_{\mathrm{List}\langle B\rangle}$

みたいな。

このリスト関手 $\mathcal F$ は確かに任意の $A,B,f$ からなる小さな部分圏を $\mathrm{List}\langle A\rangle, \mathrm{List}\langle B\rangle, \mathcal F_m(f)$ からなる別の圏構造へその構造を保ったまま移す写像になっている。

圏が十分に広い範囲の射を含むケースにおいて、
この関手は忠実である: $f\ne g$ に対して $\mathcal F_m(f)\ne \mathcal F_m(g)$ が成り立つ
この関手は充満ではない： 各要素に同一の関数を当てはめる以外のずっと多くの射、例えば要素の入れ替えなどが考えられ、$\mathcal F_m(f)$ はそれらを覆いつくさない。

忠実性や充満性は圏がどういう射を含んでいるか次第であることには注意が必要だ。そもそも $f\ne g$ となるような射が存在しないなら $\mathcal F_m$ をどう定義したところで忠実。リスト間に適用可能な関数が map しか与えられていないなら充満になりうる。

準備：積圏†

２つの圏$\mathcal{C}$と$\mathcal{D}$から、新しい圏$\mathcal{C}\times\mathcal{D}$（積圏）を以下のように作る。

• 対象：$\mathcal{C}$の対象$c$と$\mathcal{D}$の対象$d$のペア $(c,d)$
• 射：$(c,d)\to(c',d')$は、$\mathcal{C}$の射$f\colon c\to c'$と$\mathcal{D}$の射$g\colon d\to d'$のペア$(f,g)$
• 合成：成分ごとに合成する。$(f',g')\circ(f,g)=(f'\circ f,\ g'\circ g)$
• 恒等射：$(c,d)$の恒等射は$(1_{\mathcal C},1_{\mathcal D})$

2つの圏を「横に並べて、対象も射もペアにしただけ」のもの。

双関手†

双関手は２つの圏から１つの圏への写像であるが、
つまり積圏を始域とする通常の関手とみなすこともできる。

$\mathcal C\times \mathcal D\to \mathcal E$

積の双関手†

分かりやすい例は積の双関手。
この場合には $\mathcal C=\mathcal D=\mathcal E$ として、
任意の対象 $A,C$ とその間の射 $f:A\to C$
任意の対象 $B,D$ とその間の射 $g:B\to D$^ を考える。

さらにこの圏が $A\times B$ および $C\times D$ の積構造を含んでいるとして次のような絵を描くと、ここから下記の形の「積の双関手」を抽出できる。

$\mathcal F_o(A,B)=A\times B$
$\mathcal F_o(C,D)=C\times D$
$\mathcal F_m(f,g)=(a, b)\mapsto(f(a), g(b))$ これは $(A\times B)\to(C\times D)$ の写像

積構造 $A\times B$ および $C\times D$ には $A,B,C,D$ との間の射の存在が含まれているため、始めに $\mathcal C=\mathcal D=\mathcal E$ を仮定したのであった。このように、積の双関手は圏が積構造を含む際に初めから存在した構造を浮き彫りにしたものとみなせる。

余積の双関手†

同様に余積の双関手も作れる。
$\mathcal F_o(A,B)=A+B$
$\mathcal F_o(C,D)=C+D$
$\mathcal F_m(f,g)=A\text{の元なら} f \text{を、} B\text{の元なら} g \text{を適用}$ これは $(A+B)\to(C+D)$
これも余積の構造に付随して初めから存在する構造に名前を付けたものとみなせる。

これら積の双関手や余積の双関手の後ろに通常の（単項の）関手をつなぐことで、バラエティ豊かな一般の双関手を構成可能である。

反変関手・共変関手†

関手の $\mathcal F_m$ が射の向きをすべて逆転させるとき、反変関手という
今まで考えていた射の向きを保つ普通の関手は 共変関手という

$\mathcal C$ の反変関手による変換は $\mathcal C^{\mathrm{op}}$ の共変関手による変換と見做せる

プロ関手†

第1引数 $\mathcal C$ に反変、第2引数 $\mathcal D$ に共変な、Set圏を終域とする双関手をプロ関手という $$\mathcal C^{\mathrm{op}}\times\mathcal D\to\mathrm{Set}$$ なぜこんなものを考えるのか？

元々やりたいのは、

• $\mathcal C$ の射 $f_{ab}:A\to B$
• $\mathcal D$ の射 $f_{cd}:C\to D$

を元にして、

$f_{bc}:B\to C$ の前後に $f_{ab},f_{cd}$ を継ぎ足して $f_{ad}:A\to D$ に変換する射を生成するようなこと $$f_{bc}\mapsto f_{cd}\circ f_{bc}\circ f_{ab}=f_{ad}$$ $f_{cd}\circ f_{bc}\circ f_{ab}$ の接続により $A\to B\to C\to D$ として正しく計算可能になる。

この接続の演算は対象「$B\to C$ の任意の関数」から「対象 $A\to D$ の任意の関数」への射である。

これを 対象のペア $(B,C)$ から対象のペア $(A,D)$ への射 $(f_{ab}^{\mathrm{op}}, f_{cd})$ から生成する関手を考えているのだ。

変換先で必要となる情報が、正しく変換元から与えられていることを確認できる。

プロ関手で片側のみ双対をとる必要が生まれたのは、$(B,C),(A,D)$ のペアを作るためであったことが分かるはずだ。

プロ関手はこれを一般化した、
$\mathcal C^{\mathrm{op}}\times\mathcal D\to\mathrm{Set}$ の形を満たす変換のことなので、
以下の形をテンプレートとすると理解しやすい。

Hom関手†

圏 $\mathcal C(O, \mathrm{hom})$ から射の集合 hom を取り出す関手で、これは $\mathcal C$ 同士の間のプロ関手になる。 $$\mathcal C^{\mathrm{op}}\times\mathcal C\to \mathrm{Set}$$ 上の表を使うと関手の変換は以下のように理解できる。

プロ関手の説明で「こういうことがしたい」とかいていたものそのままが Hom 関手と思ってOK。

その意味するところ†

関数対象$A\Rightarrow B$とは、対象 $A,B$ を含む圏に存在する１つの対象であって、対象$A$から$B$への射の集合そのものであるか、あるいは対象$A$から$B$への射と一対一に対応する要素(個々の射に付けたラベルのようなもの)を集めた集合、であることを想定して作られた存在だ。 特定の圏が実際にそういうものを含むかどうか、あるいはそれがどのように射と対応するか、あたりも含めて以下で説明する。

まず、Set圏はすべての集合を対象として含む圏だった。
任意の集合間の写像を集めた hom は集合になるから、
Set圏の任意の hom はそれ自身Set圏に対象として存在する。
だからこれをそのまま関数対象見做せる。

一方、その他の圏では hom 集合自体が対象として存在する保証がないため、関数対象は射自身を集めたものではなく、射と一対一に対応するラベルを集めた集合であっても構わない。

公理化の方針†

以下ではこの「関数対象」に普遍的な公理（要素に言及せず射の性質のみで記述された公理）を与える。実のところ、そのような圏論的な定義は関数対象$A\Rightarrow B$ の内部構造に踏み込まないので、その要素が何であるかという上記のような話は本質的ではなくなる。

またこの公理は「圏の中に関数対象を作り出そう」とするものではない。すでに圏の全体像は決まっているものとして、その圏の個々の対象に対して、その対象が「関数対象$A\Rightarrow B$ と見做せるものであるかどうか」を判別する手段を与えるものである。

この公理、かなり複雑なので順を追って説明する。

公理の実体†

考える関数（射）の始域を $A$、終域を $B$ として、これらは圏に含まれるとする。

関数対象の候補を $Z$ とすると、関数に始域$A$の値を与えて評価し、終域$B$の値を得る手順は、具体的な関数(のラベル) $z\in Z$ と、そこに与える引数 $a\in A$ を受け取って、そこから返り値 $b\in B$ を計算して返すことに相当する。

関数対象の公理ではこの手順を $Z\times A$ から $B$ への射（評価射と呼ばれる） $g:Z\times A\to B$ と同一視するため、そもそも圏に積 $Z\times A$ が含まれないような $Z$ は始めから関数対象の候補から外してしまう。

一般には関数対象は単なるラベルなので、その評価射 $g$ とセットで初めて演算の内容が定義される。そこで以下では候補探しは $Z,g$ をセットで考える。

$Z\times A$ が存在し、評価射の候補 $g:Z\times A\to B$ が存在すれば、$Z,g$ は関数対象とその評価射の候補になる。そして、ある特定の候補が圏に含まれる任意の候補を下記の意味で「過不足なく生成可能」であるとき、それこそが関数対象$A\Rightarrow B$ および評価射 $\mathrm{eval}$ であるとするのがこの公理である。そのような候補は複数あっても構わないが、それらはすべて同型となるため、関数対象$A\Rightarrow B$は同型を除いて一意に決定される。逆にそのような候補がないとき、その圏には関数対象$A\Rightarrow B$は存在しない。

関数対象とその評価射の候補 $Z',g'$ が別の候補 $Z,g$ から「過不足なく生成可能」とは、
$$g'=g\circ(h\times 1_A)$$ を成り立たせる $$h:Z'\to Z$$ が 「ただ一つだけ」 存在すること、として定義される。

これだけだと難しいので、以下では集合の言葉を使って解釈しよう。

$g'=g\circ(h\times 1_A)$ の意味†

等号で結ばれた２つの射に $(z',a)\in Z'\times A$ を与えると、$$g'(z',a)=g\circ(h\times 1_A)\,(z',a)$$ となる。

• 左辺は $g'$ がそのまま $z'\in Z'$ を使って $a\in A$ を評価する射
• 右辺は $(h(z'),a)$ に変換してから $g$ に渡すという合成射
  つまり $g$ が $z=h(z')$ で $a$ を評価する射

これら２つが等しいという主張。
言い換えれば、$z$ と $h(z')$ が同じ関数を表すということ。

なぜこの条件を $Z,g$ が $Z',g'$ を過不足なく生成可能と言うのか？

過不足なく生成可能†

上の条件を成り立たせる $h$ の存在は、
任意の $z'\in Z'$ に対してそれと一致する関数 $h(z')$ が $Z$ に含まれていることを意味する

そして、そのような $h$ が複数存在するとしたら、
ある $z'\in Z'$ に一致する関数 $h_1(z'), h_2(z'), \dots$ が２つ以上 $Z$ に含まれており、そのうちどれ対応させてもよい、ということになる。すなわち $Z$ 内に同じ関数が複数含まれていることに対応する。

だから、そのような $h$ が「ただ１つ存在する」という主張は任意の $z'\in Z'$ に対して、それと一致する関数が $Z$ にただ一つ含まれている、と読み替えられて、これが候補 $Z',g'$ が別の候補 $Z,g$ から「過不足なく生成可能」の意味である。

すべての候補を過不足なく生成可能†

すべての候補を「過不足なく生成可能」な $Z,g$ が見つかったならそれらを $A\Rightarrow B,\mathrm{eval}$ と書き、関数対象とその評価射と呼ぶ。

上記の公理により、$A\Rightarrow B$ には圏が持つ任意の $Z\times A$ と、$\mathrm{hom}(Z\times A,B)$ に含まれる任意の評価射の組み合わせで表現しうるすべての$A\to B$関数から、重複を取り除いたうえですべて１つずつ含まれていることが保証される。

追加で必要な条件†

ここまで来て何なのだが、実はここまでの議論には致命的な欠陥がある。

すぐ上で次のように書いた。

上記の公理により、$A\Rightarrow B$ には圏が持つ任意の $Z\times A$ と、$\mathrm{hom}(Z\times A,B)$ に含まれる任意の評価射の組み合わせで表現しうるすべての$A\to B$関数から、重複を取り除いたうえですべて１つずつ含まれていることが保証される。

上記公理が $A\Rightarrow B,\mathrm{eval}$ に保証するのは本当にこれだけなのだ。

何が欠けているかと言うと、「候補たちが表現していた関数」 が 「実際の$\mathrm{hom}(A,B)$と対応しているかどうか」 について一切言及されていないのだ！

これは本当に致命的なのであるが、上記の公理に
「圏が終対象 $1$ およびその積 $1\times A$ を含むこと」という新たな仮定を加えると、
関数対象 $A\Rightarrow B$ が（圏論の意味で）正しく $\mathrm{hom}(A,B)$ と一対一に対応し、
その射を評価射 $\mathrm{eval}$ により再現できることが保証される。

（圏論の意味で）の注釈については下記証明を参照。

デカルト閉圏†

そこで、この仮定に、さらに、「関数対象の存在」まで追加で保証した圏、つまり（終対象＋任意の対象の積＋任意の対象間の関数対象）を全部備えた圏には **デカルト閉圏 (Cartesian closed category)** という名前がついており、関数対象に関する議論ではほぼ常にデカルト閉圏が暗黙のうちに仮定される。