Definition 1.4.4 (Heyting algebra). A Heyting algebra is a bounded lattice equipped with a binary operation $\Rightarrow :H\times H\to H$ such that

$$a\wedge b\le c⟺a\le (b\Rightarrow c)$$

for all $a,b,c\in L$.

A morphism of Heyting algebras is a function that preserves all finite meets, finite joins, and $\Rightarrow$.