In the following, $\leftadj{ c[\lambda] }$ is the colimit, i.e. least upper bound,
of the functor, i.e. monotone function, labeled $\rightcat z$ in the 2-D diagram.
\[ \begin{array} {} \text{2-dimensional, in $\Cat$} & \kern2em & \boxed{ \begin{array} {} && \rightcat 1 && {} \rlap{ \rightcat{ \kern-3em \xrightarrow[\kern8em] {\textstyle y} } } && \rightcat H & \kern3em \\ & \rightcat{ \llap ! \nearrow } & \smash{ \leftadj{ \llap \lambda \Big\Uparrow } } & \leftadj{ \llap c \searrow } & \smash{ \rightadj{\Big\Uparrow} \rlap{ \rightcat y \rightadj\epsilon } } {} \rlap{ \kern-3em \smash{ \rightcat{ \Bigg\Uparrow } } } & \leftadj{ \nearrow \rlap {L = (\leftcat{-} \wedge x)} } \\ \leftadj{ (\leftcat{-} \wedge x) } \rightcat{ {} \downarrow y } && \leftcat{ {} \rlap{ \kern-3em \xrightarrow [\textstyle z] {\kern8em} } } && \leftcat H \end{array} } \\ \\ \\ \text{1-dimensional, in $H$} && \boxed{ \begin{array} {} \kern0em & \leftadj c && \rightcat y && \leftadj x \\ & \smash{ \raise0ex{ \leftadj{ \llap{ \lambda_{\leftcat z} } \big\uparrow } } } & \rightadj\nwarrow & \smash{ \raise0ex{ \rightadj{ \big\uparrow \rlap{ \rightcat y \epsilon } } } } & \rightadj\nearrow & \smash{ \raise0ex{ \leftadj{ \big\Vert } } } \\ & \leftcat z && \leftadj{ c \wedge x } && \leftadj x \\ & & \rightadj\nwarrow & \smash{ \raise0ex{ \big\uparrow \rlap{ \kern-1.87em \leftadj{ \lambda_{\leftcat z} \wedge x } } } } & \rightadj\nearrow \\ & && \leftadj{ \leftcat z \wedge x } \end{array} } \\ \\ \\ \text{0-dimensional, in $\Omega$} && \boxed{ \begin{array} {} \rightcat{ \leftadj{ \leftcat z \wedge x } \leq y } & \xrightarrow{\textstyle \leftadj c \text{ an upper bound} } & \rightcat{ \leftcat z \leq \leftadj c } \\ \leftcat{ z \leq \leftadj c } & \xrightarrow{ \textstyle \leftadj{ \leftcat - \wedge x } } & \leftadj{ \leftcat z \wedge x \leq c \wedge x \buildrel \rightcat y \rightadj\epsilon \over { \mathrel{ \rightadj\leq } } \rightcat y } \end{array} } \end{array} \]
Thus $\leftadj c[\rightcat y \rightadj\epsilon]$ is a terminal object in $ \leftadj{ (\leftcat{-} \wedge x) } \rightcat{ {} \downarrow y }$,
so $\leftadj c$ is an instance of the general categorical notion of "internal hom", often denoted $\rightadj{ [\leftadj x , \rightcat y] }$ or ${\rightcat y}^{\leftadj x}$.
In the case of Heyting algebras, it is commonly denoted $\leftadj x { \rightadj\Rightarrow } \rightcat y$, showing that it is an internalization of implication.
(To see this, take $\leftcat z = \rightadj\top$ in the above diagrams.)
Another notation, useful when the product operation (here meet $\wedge$) is not symmetic, is $\leftadj x { \rightadj\backslash } \rightcat y$.
Reference
Mac Lane and Moerdijk SGL I.8
