ηP:P→P+ が単射であるとは、 任意の対象 C に対して ηPC:PC→P+C が単射であるということである。 ここで、 各対象 C に対し、 定義から ηPC=i⊤C∘yPC であって yPC は同型射だから、 ηPC が単射であることと i⊤C が単射であることは同値である。 したがって、 P が分離前層であることと、 任意の対象 C に対して i⊤C:Hom(⊤C,P)→P+C が単射であることが同値になることを示す。

P が分離前層であると仮定する。 任意の対象 C をとり、 射 a,a󰎘:⊤C→P が i⊤Ca=i⊤Ca󰎘 を満たすとする。 これは、 P+C を定める同値関係において a,a󰎘 が同値であるということなので、 ある被覆篩 S∈JC が存在して a∘S=a󰎘∘S が成り立つ。 仮定から P は分離前層なので -∘S は単射であるから、 これより a=a󰎘 を得る。 以上で、 i⊤C は単射である。

逆に、 任意の対象 C に対して i⊤C が単射であると仮定する。 任意の被覆篩 S∈JC に対し、 Hom(⊤C,P)P+CHom(S,P)i⊤C-∘SiS は可換であるが、 仮定から i⊤C は単射なので -∘S も単射である。 よって、 P は分離前層である。

命題 3.2 のときと同様に、 P が層であることと、 任意の対象 C に対して i⊤C:Hom(⊤C,P)→P+C が全単射であることが同値になることを示す。

P が層であると仮定する。 任意の対象 C をとる。 元 α∈P+C をとり、 これがある被覆篩 S∈JC に対して a:S→P で代表されるとすると、 α=iSa である。 仮定から P は層なので -∘S は全単射であるから、 ある a󰎘:⊤C→P が存在して a=a󰎘∘S が成り立つ。 したがって α=iS(a󰎘∘S)=i⊤Ca󰎘 であるから、 i⊤C が全射であることが示された。 命題 3.2 によって i⊤C はすでに単射なので、 i⊤C は全単射である。

逆に、 任意の対象 C に対して i⊤C が全単射であると仮定する。 任意に被覆篩 S∈JC をとり、 さらに射 a:S→P をとる。 仮定から i⊤C が全単射なので、 ある a󰎘:⊤C→P が存在して iSa=i⊤Ca󰎘 が成り立つ。 これは、 P+C において a,a󰎘 が同値であるということなので、 ある被覆篩 T∈JC が存在し、 T⊆S であって、 STP⊤Caa󰎘 が可換である。 ここで、 任意の射 f∈S:D→C に対し、 図式 f∗TyDSPTyDyD⊤CPyCf∘-f∘-af∘-f∘-a󰎘 を考えると、 左の四角形は f∗T の定義によって可換であり、 上下の三角形は明らかに可換で、 折れ曲がった長方形は上の図式と同じものなので可換である。 したがって、 横に長い長方形も可換である。 ここで、 命題 3.2 によって P が分離前層であることは分かっているので、 写像 -∘f∗T:Hom(yD,P)→Hom(f∗T,P) は単射である。 この事実と上の図式の可換性を踏まえると、 SyDP⊤Cf∘-f∘-aa󰎘 が可換であることが分かる。 この図式において idD の行き先を見ることで、 aDf=aD󰎘f が得られる。 f は S に属する任意の射であったから、 これによって a=a󰎘∘S が得られ、 -∘S が全射であることが示された。 命題 3.2 によって -∘S はすでに単射なので、 -∘S は全単射となり、 P は層である。

任意の対象 C とそれ上の被覆篩 S∈JC をとる。 F は層であるから、 包含射による写像 -∘S:Hom(yC,F)→Hom(S,F) は全単射であり、 したがって逆写像をもつ。 これを用いて、 合成 Hom(S,P)Hom(S,F)Hom(yC,F)FCφ∘-(-∘S)−1yFC−1 を考えると、 これらは関手 Hom(-,P):JC∘→Set の余錐となる。 したがって、 この余極限である P+C からの一意的な射 󰔃φC:P+C→FC が存在する。 これは C に関して自然なので、 自然変換 󰔃φ:P+→F が得られる。

さて、 定義によって、 各対象 C に対し、 Hom(S,P)P+CHom(S,F)Hom(yC,F)FCφ∘-iS󰔃φC(-∘S)−1yFC−1 は可換である。 ここで特に S=⊤C とおけば、 図式 PCHom(⊤C,P)P+CFCHom(yC,F)FCyPCφCi⊤Cφ∘-󰔃φCyFCyFC−1 の右側の四角形の可換性が得られるが、 この左側の四角形も明らかに可換なので、 全体も可換である。 これはすなわち、 ここで構成した 󰔃φ:P+→C が命題の主張の図式を可換にしていることを意味する。

󰔃φ の一意性は、 余極限が誘導する射の一意性から従う。

前層 P:󰒚∘→Set に対し、 合成 PP+P++ηPηP+ を 󰔄ηP とおく。 命題 3.4 を 2 回使うことで、 任意の層 F:󰒚∘→Set への自然変換 φ:P→F は、 PaPF󰔄ηPφ󰔃φ を可換にする自然変換 󰔃φ によって、 󰔄ηP を通して一意的に分解される。 これは、 定理の主張にある随伴が、 󰔄η を単位として成立することを意味する。