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
