󰒛 の対象 D に対し、 コンマ圏 D↓F を考える。 これは次のような圏である。

• D↓F の対象は、 󰒚 の対象 C および 󰒛 の射 f:D→FC の組 (C,f) である。
• D↓F の 2 つの対象 (C,f),(C󰎘,f󰎘) の間の射は、 󰒚 の射 h:C→C󰎘 であって、 図式 DFCFC󰎘ff󰎘Fh を可換にするものである。

このコンマ圏を用いて、 関手 ∃F を次のように定義する。 ∃F: Set󰒚∘ ⟶ Set󰒛∘ P ⟼ ❲ 󰒛∘ ⟶ Set D ⟼ colim(C,f)∈D↓FPC❲ 󰒚 が小圏で 󰒛 が局所小圏であることから D↓F は小圏であり、 Set は余完備であるから、 式中の余極限は常に存在する。 この ∃F が F∗ の左随伴関手を与える。 それを示すには、 Set󰒚∘ の対象 P と Set󰒛∘ の対象 Q に対し、 集合としての自然な同型 HomSet󰒚∘(P,F∗Q)≅HomSet󰒛∘((∃F)P,Q)♡ を示せば良い。

まず、 左辺の集合の元 (すなわち自然変換) α:P⇒F∗Q をとる。 󰒛 の対象 D および D↓F の対象 (C,f) に対し、 θD(C,f):=Qf∘αC:PC→QD とおく。 ここで、 任意の D↓F の射 h:(C,f)→(C󰎘,f󰎘) に対して、 図式 PC󰎘PCQFC󰎘QFCQDαC󰎘αCPhQf󰎘QfQFh は可換であるが、 この図式の外側の可換性は θD(C,f) たちが colim(C,f)PC に関する余錐であることを意味している。 したがって、 余極限の普遍性によって、 写像 βD:colim(C,f)PC→QD が得られる。 これは D に関して自然であることが容易に確かめられるので、 自然変換 β:(∃F)P⇒Q が得られた。

逆に、 自然変換 β:(∃F)P⇒Q が与えられたとする。 これは、 󰒛 の各対象 D に対して、 写像 βD:colim(C,f)PC→QD が定まっているものである。 さらに余極限の構造射との合成により、 D↓F の各対象 (C,f) に対して、 射 θD(C,f):PC→QD が得られる。 ここで、 特に D:=FC および f:=idFC とおけば、 射 αC:=θFC(C,id):PC→QFC が得られる。 これは C に関して自然であることが容易に確かめられるので、 自然変換 α:P⇒F∗Q が得られた。 以上の構成は互いに逆になっているので、 式 ♡ が示された。

なお、 右随伴関手 ∀F の構成は同様であるため省略する。

随伴 F⊣G の余単位を ε:F∘G⇒id󰒛 とおくと、 P との合成によって、 Set󰒚∘ の射 ηP󰎘:=P∗ε:P→P∘F∘G が得られる。 P∘F∘G=G∗F∗P であり、 上の射は P に関して自然だから、 自然変換 η󰎘:idSet󰒚∘⇒G∗∘F∗ が誘導される。 同様にして、 随伴 F⊣G の単位 η:id󰒚⇒G∘F からは、 自然変換 ε󰎘:F∗∘G∗⇒idSet󰒚∘ が誘導される。 さらに、 η と ε が随伴の三角可換図式を満たすことから、 η󰎘 と ε󰎘 も随伴の三角可換図式を満たすことが従う。 以上により、 F∗⊣G∗ が成り立つ。

記号の簡略化のため P󰒚:=Set󰒚∘ とおく。 PP󰒚 の対象 Φ と P󰒚 の対象 P に対し、 集合としての自然な同型 HomP󰒚(Y∗Φ,P)≅HomPP󰒚(Φ,ZP)♡ を示せば良い。

左辺の集合の元 α:Y∗Φ⇒P をとる。 P󰒚 の対象 R および 󰒚 の対象 C に対し、 ΦR の元 a および RC の元 b をとる。 Yoneda の補題によって RC≅Hom(YC,R) が成り立つから、 この全単射を通して b と対応する射を 󰂡b:YC→R とおく。 すると、 hR,Cb:=αC∘Φ󰂡b:ΦR→PC が得られるから、 この写像による a の像を b に対応させる写像として、 γR,Ca: QC ⟶ PC b ⟼ hR,Cba が定義できる。 これは C に関して自然であることが分かるので、 自然変換 γRa:R⇒P が得られる。 すると、 これを a に対応させる写像として、 ξR: ΦR ⟶ HomP󰒚(R,P) a ⟼ γRa が定義できる。 Hom(R,P)=(ZP)R であることと、 この写像が R に関して自然であることから、 自然変換 ξ:Φ⇒ZP が得られた。

逆に、 自然変換 ξ:Φ⇒ZP が与えられたとする。 󰒚 の対象 C に対して、 Yoneda の補題により (ZP)(YC)=Hom(YC,P)≅PC であるから、 この自然変換の YC-成分は、 αC:=ξYC:ΦYC→PC という形の写像を与える。 これは C に関して自然であるから、 自然変換 α:Y∗Φ⇒P が得られた。 以上の構成は互いに逆になっているので、 式 ♡ が示された。

以下、 圏 󰒚 上の Yoneda 埋め込み関手を Y󰒚:󰒚→Set󰒚∘ で表すことにする。 また、 対象と射を全くもたない圏を 0 で表し、 対象と射をそれぞれ 1 つしかもたない圏を 1 で表す。

まず Y0 に補題 2 を適用すると ∃Y0⊣Y0∗ が得られる。 さらに補題 4 を適用すれば Y0∗⊣YSet0∘ が得られる。 ところで Set0∘≅1 であるから、 最終的に ∃Y0⊣Y0∗⊣Y1 が得られたことになる。

この随伴列に補題 3 を適用すると (∃Y0)∗⊣Y0∗∗⊣Y1∗ が得られる。 さらにこの両端の関手について、 補題 2 によって ∃∃Y0⊣(∃Y0)∗ が得られ、 補題 4 によって Y1∗⊣YSet1∘ が得られる。 ところで Set1∘≅Set であることから、 結局、 ∃∃Y0⊣(∃Y0)∗⊣Y0∗∗⊣Y1∗⊣YSet が示され、 この随伴列が存在を示したかったものである。