For 𝜗 ∈𝖯𝖲𝗁(𝖢)(よ𝑋,𝐹) we have 𝜗𝑋 :𝖢(𝑋,𝑋) →𝐹𝑋. Let 𝑥𝜗 :=𝜗𝑋(1𝑋) ∈𝐹𝑋.

Conversely, given an 𝑥 ∈𝐹𝑋, we can define 𝜗𝑥 :よ𝑋 ⇒𝐹 :𝖢𝐨𝐩 →𝖲𝖾𝗍 as follows: Given any 𝑋′, we define the component

whose naturality condition is given by the diagram

Now for ℎ ∈𝖢(𝑋′,𝑋) we have

so 𝜗𝑥 is indeed natural.

Now we calculate 𝜗𝑥𝜗 for 𝜗 ∈𝖯𝖲𝗁(𝖢)(よ𝑋,𝐹). From the above definitions, for ℎ ∈𝖢(𝑋′,𝑋) we have

but by naturality of 𝜗

wherefore 𝜗(𝑥𝜗) =𝜗.

Conversely, for 𝑥 ∈𝐹𝑋 we have

Therefore

defines a bijection for any 𝑋,𝐹.

For naturality in 𝐹, suppose 𝜗 ∈𝖯𝖲𝗁(𝖢)(𝐹,𝐺) Then for any 𝜑 ∈𝖯𝖲𝗁(𝖢)(よ𝑋,𝐹) we have

so the required diagram commutes.

For naturality in 𝑋, suppose ℎ ∈𝖢(𝑋,𝑌). Then for 𝜓 ∈𝖯𝖲𝗁(𝖢)(よ𝑌,𝐹) we have

as required.