証明.

CAAccNF の対象 SetA,SetB に対し、 その積と冪は、 SetA×SetB = SetA+B SetA⇀SetB = SetexpA×B で与えられる。 積が上の形で与えられることは明らかなので、 冪が上の形で与えられることを示す。

CAAccNF の別の対象 SetC に対し、 定理 4.7 を用いると、 圏同値 [SetC,SetexpA×B]NF ≅ SetexpC×(expA×B) ≅ Setexp(C+A)×B ≅ [SetC+A,SetB]NF = [SetC×SetA,SetB]NF が成立することが分かる。 これはすなわち、 集合としての同型 HomCAAccNF(SetC,SetexpA×B)≅HomCAAccNF(SetC×SetA,SetB) が成り立つことを意味している。 したがって、 冪は上に示した形で与えられる。

証明.

簡単のため C:=expA×B とおく。 上の証明の圏同値 [SetC,SetC]NF ≅ SetexpC×C ≅ Setexp(C+A)×B ≅ [SetC+A,SetB]NF = [SetC×SetA,SetB]NF において、 idSetC∈[SetC,SetC]NF と対応するものが求めたい余単位である。

まず、 最初の圏同値で idSetC と対応するのは、 N: expC×C ⟶ Set (δ,c) ⟼ { 1 (δ={c}) 0 (上記以外) である。 実際、 各 c∈C と M∈SetC に対し、 N󰂦cM = 󰄘δ∈expC(Hom(δ,M)×N(δ,c)) ≅ Hom({c},M) ≅ Mc であるから、 N󰂦=idSetC である。

次の圏同値でこの N と対応するのは、 同じ記号を使うが、 N: exp(C+A)×B ⟶ Set (ϵ,b) ⟼ { 1 (ϵ=γ∪{(γ,b)},γ∈expA) 0 (上記以外) である。 このことは、 全単射 expC×(expA×B) ⟶ exp(C+A)×B (δ,(γ,b)) ⟼ (δ∪γ,b) を考えれば明らかである。

さらに次の圏同値でこの N と対応するものは、 各 b∈B に対し、 N󰂦b: SetC+A ⟶ Set Y ⟼ 󰄘ϵ∈exp(C+A)(Hom(ϵ,Y)×N(ϵ,b)) で与えられるが、 これは、 N󰂦b: SetC×SetA ⟶ Set (M,X) ⟼ 󰄘γ∈expA(Hom(γ,X)×M(γ,b)) とも書ける。 実際、 最初の表示の余積においては、 γ∈expA に対して ϵ=γ∪{(γ,b)} という形の場合しか考えなくて良く、 このとき、 Hom(γ∪{(γ,b)},(M,X))≅Hom(γ,X)×M(γ,b) が成り立つから、 上の 2 つの表示は等しい。 さらに、 上の 2 つ目の表示の右辺は M󰂦bX そのものである。 以上により、 命題が示された。