󰒚 の対象 B,C に対し、 合成 [B,C]⊗󰄖A∈󰒚[FA,GA][FB,FC]⊗[FC,GC][FB,GC]FBC⊗prCcFB,FC,GC とテンソル積の随伴で対応する射を pBC:󰄖A∈󰒚[FA,GA]⟶[B,C]⊸[FB,GC] とおく。 この射たちは、 p:󰄖A∈󰒚[FA,GA]⟶󰄖B,C∈󰒚([B,C]⊸[FB,GC]) を定める。 同様にして、 󰒚 の対象 B,C に対し、 合成 󰄖A∈󰒚[FA,GA]⊗[B,C][FB,GB]⊗[GB,GC][FB,GC]prB⊗GBCcFB,GB,GC とテンソル積の随伴で対応する射を qBC:󰄖A∈󰒚[FA,GA]⟶[B,C]⊸[FB,GC] とおき、 これらが定める射を q:󰄖A∈󰒚[FA,GA]⟶󰄖B,C∈󰒚([B,C]⊸[FB,GC]) とする。 これによって平行な射が 2 本できたので、 等化子 N󰄖A∈󰒚[FA,GA]󰄖B,C∈󰒚([B,C]⊸[FB,GC])pq を計算する。 この N が存在を示したい対象になっている。

実際、 Hom(1,-):󰒭→Set は表現可能関手なので極限を保存するため、 Hom(1,N)󰄖A∈󰒚Hom(1,[FA,GA])󰄖B,C∈󰒚Hom(1,[B,C]⊸[FB,GC])p∘-q∘- は Set で等化子の図式になっている。 したがって、 同型の違いを除いて Hom(1,N) は、 󰒚 の対象 A に対する射 γA:1→[FA,GA] たちの族 (γA)A∈󰒚 であって、 p∘(γA)A∈󰒚=q∘(γA)A∈󰒚 を満たすもの全体の集合である。 この等式は、 任意の 󰒚 の対象 B,C に対して、 pBC∘(γA)A∈󰒚=qBC∘(γA)A∈󰒚 が成り立つのと同値である。 さらにこの等式は、 テンソル積の随伴で対応する射を考えることにより、 [B,C]⊗1[B,C]⊗󰄖A∈󰒚[FA,GA][FB,FC]⊗[FC,GC][FB,GC]1⊗[B,C]A∈󰒚󰄖A∈󰒚[FA,GA][FB,GB]⊗[GB,GC]id⊗γσ[B,C],1FBC⊗prCcFB,FC,GCγ⊗idprB⊗GBCcFB,GB,GC の可換性と同値である。 この図式を少し書き換えれば、 [B,C]⊗1[FB,FC]⊗[FC,GC][FB,GC]1⊗[B,C][FB,GB]⊗[GB,GC]FBC⊗γCσ[B,C],1cFB,FC,GCγB⊗GBCcFB,GB,GC♡ となり、 これは γ の自然性を表す図式そのものである。 以上により、 Hom(1,N)≅{󰒭-豊穣自然変換 γ:F⇒G} が成り立つ。

󰒭-豊穣関手 F,G:󰒚→󰒛 の間の射対象を、 命題 3.2 の ⟦F,G⟧ とする。 あとは合成を表す射と恒等射を与える射を構成すれば良い。

まず、 󰒭-豊穣関手 F,G,H:󰒚→󰒛 に対して射 cFGH:⟦F,G⟧⊗⟦G,H⟧→⟦F,H⟧ を構成する。 󰒚 の対象 A に対し、 ⟦F,G⟧󰄖A∈󰒚[FA,GA][FA,GA]prA を mA とおく。 なお、 この合成における最初の射は、 等化子としての ⟦F,G⟧ の構造射である。 同様にして、 ⟦G,H⟧󰄖A∈󰒚[GA,HA][GA,HA]prA を nA とおく。 これらの射を用いて、 ⟦F,G⟧⊗⟦G,H⟧[FA,GA]⊗[GA,HA][FA,HA]mA⊗nAcFA,GA,HA を考え、 これを sA とおく。 この sA たちは、 s:⟦F,G⟧⊗⟦G,H⟧⟶󰄖A∈󰒚[FA,HA] を定める。

さて、 任意に 󰒚 の対象 B,C をとる。 まず ⟦F,G⟧ について、 命題 3.2 で図式 ♡ の可換性を導いたのと同様にして、 [B,C]⊗⟦F,G⟧[FB,FC]⊗[FC,GC]⟦F,G⟧⊗[B,C][FB,GB]⊗[GB,GC][FB,GC]FBC⊗mCσ[B,C],⟦F,G⟧cFB,FC,GCmB⊗GBCcFB,GB,GC♤ が可換であることが分かる。 したがって、 [B,C]⊗⟦F,G⟧⊗⟦G,H⟧[B,C]⊗⟦F,G⟧⊗[GC,HC][FB,FC]⊗[FC,GC]⊗[GC,HC]⟦F,G⟧⊗[B,C]⊗⟦G,H⟧⟦F,G⟧⊗[B,C]⊗[GC,HC]⟦F,G⟧⊗[GB,GC]⊗[GC,HC][FB,GB]⊗[GB,GC]⊗[GC,HC][FB,GC]⊗[GC,HC]⟦F,G⟧⊗[GB,HC][FB,GB]⊗[GB,HC][FB,HC]id⊗nσ⊗idF⊗m⊗idσ⊗idc⊗idid⊗G⊗nm⊗G⊗idm⊗idid⊗cc⊗idid⊗ccm⊗idc は可換である。 実際、 右上の矩形部分は上の図式から可換であり、 右下の矩形部分は合成の結合性から可換で、 それ以外の部分はテンソル積の関手性から可換である。 したがって、 [B,C]⊗⟦F,G⟧⊗⟦G,H⟧[B,C]⊗⟦F,G⟧⊗[GC,HC][FB,FC]⊗[FC,GC]⊗[GC,HC]⟦F,G⟧⊗[B,C]⊗⟦G,H⟧⟦F,G⟧⊗[GB,GC]⊗[GC,HC]⟦F,G⟧⊗⟦G,H⟧⊗[B,C][FB,GC]⊗[GC,HC]⟦F,G⟧⊗[GB,HC]⊗[HB,HC]⟦F,G⟧⊗[GB,HC][FB,GB]⊗[GB,HC]⊗[HB,HC][FB,GB]⊗[GB,HC][FB,HC]id⊗nσ⊗idF⊗m⊗idc⊗idid⊗σid⊗G⊗nid⊗cid⊗n⊗Hcm⊗idid⊗cm⊗idid⊗cc も可換になる。 実際、 左中央の矩形部分は図式 ♤ が可換であるのと同様にして可換であり、 左下の矩形部分はテンソル積の関手性から可換で、 右側の残りの部分は上の図式の外周そのものである。 そして、 この図式の外周は、 [B,C]⊗(⟦F,G⟧⊗⟦G,H⟧)[FB,FC]⊗[FC,HC](⟦F,G⟧⊗⟦G,H⟧)⊗[B,C][FB,HB]⊗[HB,HC][FB,HC]FBC⊗sCσ[B,C],⟦F,G⟧⊗⟦G,H⟧cFB,FC,HCsB⊗HBCcFB,HB,HC と書き換えられるから、 この図式も可換である。 すなわち、 ⟦F,H⟧ を等化子として定義するときに用いた 2 つの平行な射を p,q とすれば、 p∘s=p∘q が成り立つ。 よって、 等化子の普遍性により、 図式 ⟦F,H⟧󰄖A∈󰒚[FA,HA]󰄖B,C∈󰒚([B,C]⊸[FB,HC])⟦F,G⟧⊗⟦G,H⟧pqs の左側の三角形部分を可換にする破線の射が唯一存在する。 これを cFGH と定めれば良い。

次に、 󰒭-豊穣関手 F:󰒚→󰒛 に対して射 jF:1→⟦F,F⟧ を構成する。 任意の 󰒚 の対象 B,C に対し、 図式 [B,C]⊗1[FB,FC]⊗[FC,FC]1⊗[B,C][FB,FB]⊗[FB,FC][FB,FC]FBC⊗jFCσ[B,C],1cFB,FC,FCjFB⊗FBCcFB,FB,FC を考えると、 これは明らかに可換である。 したがって、 󰒚 の各対象 A に対して、 󰒛 の恒等射を定める射 jFA:1→[FA,FA] たちが定める射を t:1⟶󰄖A∈󰒚[FA,FA] とおけば、 上の議論と同様にして、 図式 ⟦F,F⟧󰄖A∈󰒚[FA,FA]󰄖B,C∈󰒚([B,C]⊸[FB,FC])1pqt の左側の三角形部分を可換にする破線の射が唯一存在する。 これを jF と定めれば良い。

以上のデータにより、 󰒭-豊穣関手とその間の 󰒭-豊穣自然変換は 󰒭-豊穣圏を成す。 本来は合成の結合性なども示さなければならないが、 それを確認する気力が今はないので、 ここでは省略することにする。