Cはデカルト閉圏だとしましょう。デカルト積とその単位(終対象)をそれぞれ、×、1 で表します。指数は BA、または [A, B] と書くことにします。
次のような指数法則は、形の上で自然に見えます(イコールは同型と解釈します)。
- A1 = A
- CA×B = (CA)B
例えば二番目の CA×B = (CA)B を確認するとしましょう。上付きは書くのが面倒なので、指数をブラケットで書くことにすれば、[A×B, C] = [B, [A, C]] です。カリー/ハワード対応があるので、指数法則は次の推論が妥当であることを意味しています。
A∧B ⊃ C
--------------
B ⊃ (A⊃C)
B ⊃ (A⊃C)
--------------
A∧B ⊃ C
あるいは、シーケントで書いて、A∧B ⊃ C ⇒ B ⊃ (A⊃C) と B ⊃ (A⊃C) ⇒ A∧B ⊃ C を示せばいいことになります。論理の証明図を書いて、それをデカルト閉圏Cで再解釈すれば、指数法則を与える具体的な同型が構成できるはずです。で、やってみると … 「アンレー?」とか嘆いて挫折。
具体的に構成できなくても(構成できるはずですけど)、米田の補題を使えば、同型であるという事実は示せてしまいます。XをCの任意の対象として、ホムセット C(X, [A×B, C]) と C(X, [B, [A, C]]) のあいだの同型を系統的に構成できれば、[A×B, C] と [B, [A, C]] が同型であることが従います。ホムセットの同型は、おおよそ次の手順で示せます。
C(X, [A×B, C])
------------------------
C(X×A×B, C)
------------------------
C(X×B×A, C)
------------------------
C(X×B, [A, C])
------------------------
C(X, [B, [A, C]])
ホムセット同型を作る手順を分析すれば、具体的な射の構成も分かるはずなのですが、ホムセット同型のほうがはるかに簡単に出来ます(少なくとも僕にとっては)。ホムセット同型が示せると「オーケイ、これでいいや」と思って、具体的な構成をそれ以上考える気力が失せます。いいんだか悪いんだか。
なぜ、ホムセット同型から対象の同型が言えるのでしょうか? その背景は米田の補題です。ここから先では、Cは単なる圏とします。圏Cの対象Aに対して、A~ を次のように定義します。
- A~(X) = C(X, A)
ここで、XはCは任意の対象です。無名のラムダ変数'-'(ブランク)を使うと A~(-) = C(-, A) と書けます。A~ は、 (Cの対象) |→ 集合 という対応ですが、f:X→Y in C に対して、
- A~(f):A~(Y) → A~(X)
という対応も定義できます。具体的には、u∈A~(Y) に対して、A~(f)(u) := f;u (手前にfを結合)とするだけです。A~ は、
- Cの対象Xに、集合C(X, A) を対応させる。
- Cの射 f:X→Y に、集合C(Y, A) から集合 C(X, A) への写像を対応させる。
そして関手性を持つので A~:C→Set (反変) という関手となります。
さらに対象Aを動かすことにより、A |→ A~ は (Cの対象)→(C→Set の反変関手) という対応になります。k:A→B があると、A~⇒B~ という自然変換をうまく定義できるので、(-)~ は、圏C → 関手圏[Cop, Set] という関手となります。
米田の補題は、米田埋め込みと呼ばれるこの関手 C → [Cop, Set] が充満忠実(full and faithful)であると主張します。つまり、次の2つの集合のあいだに(系統的な)同型があります。
- Cのホムセット C(A, B)
- 自然変換の集合 Nat(A~, B~: Cop→Set)
これから、Nat(A~, B~) のなかに自然同値が見つかれば、C(A, B) のなかに対応する同型射が存在することが保証されます。ときに、ホムセット C(A, B) より、自然変換の集合 Nat(A~, B~) のほうが見やすい/扱いやすいこともあるのです。そのようなときは、自然同値を構成できれば、具体的な射を示さなくても「オーケイ、これでいいや」となるわけです。