Arrow category ($[2,\mathcal{C}]$)

The arrow category of $\mathcal{C}$ has morphisms $A_0\to A_1$ of $\mathcal{C}$ as objects and commutative squares as morphisms. It is the functor category $[2,\mathcal{C}]$, where $2$ is the category with one nonidentity arrow.

It is also the comma category $({\mathrm{id}}_{\mathcal{C}}\downarrow {\mathrm{id}}_{\mathcal{C}})$.

Write a presheaf on $0\to 1$ as an arrow $r:B\to A$. Evaluation $\Gamma (r)=B$ has the displayed chain, where $\Pi (r)=A$, $\Delta (S)=(S\stackrel{1}{\to }S)$, $\nabla (S)=(S\to 1)$ 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 \to 1)$ is not $(\varnothing \to \varnothing )$.

The category of injective functions is the full subcategory of $[2,\mathbf{Set}]$ whose objects are injective functions. It is cartesian closed: products are computed pointwise, and exponentiating an injection by any arrow again gives an injection.