DIAGONAL ARGUMENTS AND CARTESIAN CLOSED CATEGORIES 在一個 cartesian closed category 中，如果 A→ϕBAA \xrightarrow{\phi} B^AAϕBA 是 point-surjective，則所有 B→fBB \xrightarrow{f} BBfB 都存在不動點 1→sB1 \xrightarrow{s} B1sB（滿足 f∘s=sf \circ s = sf∘s=s）。 Proof [local-0] 首先畫出交換圖 其中 δ\deltaδ 的定義是 c↦⟨c,c⟩c \mapsto \langle c, c \ranglec↦⟨c,c⟩，所以對 1→pA1 \xrightarrow{p} A1pA 來說 δ∘p=⟨p,p⟩\delta \circ p = \langle p, p \rangleδ∘p=⟨p,p⟩。沿著這個定義，我們知道 (ϕ×1A)∘δ∘p=ϕ∘⟨p,p⟩(\phi \times 1_A) \circ \delta \circ p = \phi\circ \langle p, p\rangle(ϕ×1A)∘δ∘p=ϕ∘⟨p,p⟩。根據 point-surjective 我們知道 ϕ∘p\phi \circ pϕ∘p 對每個 ppp 來說都是唯一確定的。現在把往下方 BBB 的 evevev 也畫出，即可得出等式： f∘ev∘ϕ∘⟨p,p⟩=ev∘ϕ∘⟨p,p⟩f \circ ev \circ \phi\circ \langle p, p\rangle = ev \circ \phi\circ \langle p, p\ranglef∘ev∘ϕ∘⟨p,p⟩=ev∘ϕ∘⟨p,p⟩ 換句話說 B→fBB \xrightarrow{f} BBfB 的不動點即是 ev∘ϕ∘⟨p,p⟩ev \circ \phi\circ \langle p, p\rangleev∘ϕ∘⟨p,p⟩
首先畫出交換圖 其中 δ\deltaδ 的定義是 c↦⟨c,c⟩c \mapsto \langle c, c \ranglec↦⟨c,c⟩，所以對 1→pA1 \xrightarrow{p} A1pA 來說 δ∘p=⟨p,p⟩\delta \circ p = \langle p, p \rangleδ∘p=⟨p,p⟩。沿著這個定義，我們知道 (ϕ×1A)∘δ∘p=ϕ∘⟨p,p⟩(\phi \times 1_A) \circ \delta \circ p = \phi\circ \langle p, p\rangle(ϕ×1A)∘δ∘p=ϕ∘⟨p,p⟩。根據 point-surjective 我們知道 ϕ∘p\phi \circ pϕ∘p 對每個 ppp 來說都是唯一確定的。現在把往下方 BBB 的 evevev 也畫出，即可得出等式： f∘ev∘ϕ∘⟨p,p⟩=ev∘ϕ∘⟨p,p⟩f \circ ev \circ \phi\circ \langle p, p\rangle = ev \circ \phi\circ \langle p, p\ranglef∘ev∘ϕ∘⟨p,p⟩=ev∘ϕ∘⟨p,p⟩ 換句話說 B→fBB \xrightarrow{f} BBfB 的不動點即是 ev∘ϕ∘⟨p,p⟩ev \circ \phi\circ \langle p, p\rangleev∘ϕ∘⟨p,p⟩
