Adjoint chain for evaluation in an arrow category (source code)

= Adjoint chain for evaluation in an arrow category
{title2=$\Lambda\dashv\Pi\dashv\Delta\dashv\Gamma\dashv\nabla$}

Write a presheaf on $0\to1$ as an arrow $r:B\to A$. Evaluation $\Gamma(r)=B$ has the displayed chain, where $\Pi(r)=A$, $\Delta(S)=(S\xrightarrow1 S)$, $\nabla(S)=(S\to1)$ and $\Lambda(S)=(\varnothing\to S)$. The Hom-set bijections follow by solving the commuting-square equation. The functor $\nabla$ has no right adjoint because it fails to preserve the initial object: $\nabla(\varnothing)=(\varnothing\to1)$ is not $(\varnothing\to\varnothing)$.