Heyting algebras

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