Heyting Algebra

A Heyting algebra is a Bounded Lattice $(L,\leq,\land,\lor)$ which is equipped with an internal implication operator $\Rightarrow:L^{op}\times L\to L$ such that $x\Rightarrow-$ is Right Adjoint to $x\times-$. Explicitly, this means that $x\land y\leq z$ if and only if $x\leq y\Rightarrow z$.

Properties

• Heyting algebras are a decategorification of Cartesian Closed Categories with Finite Coproducts.