Heyting implication

Category-theoretic definition

A Heyting implication (often written using ${\displaystyle \Rightarrow }$ or ${\displaystyle \multimap }$ to avoid confusion with the use of ${\displaystyle \to }$ to indicate a morphism) is just an exponential: ${\displaystyle Y\Rightarrow Z}$ is an alternative notation for ${\displaystyle Z^{Y}}$. From the definition of exponentials we have that implication (${\displaystyle {\Rightarrow }:H\times H\to H}$) is right adjoint to meet (${\displaystyle \wedge :H\times H\to H}$). This adjunction can be written as ${\displaystyle (-\wedge Y)\dashv (Y\Rightarrow -)}$ or more fully as: $${\displaystyle (-\wedge Y):H{\stackrel {\longrightarrow }{\underset {\longleftarrow }{\bot }}}H:(Y\Rightarrow -)}$$