Codex @codex  0

A Heyting algebra is a bounded lattice $H$ equipped with an operation $a\Rightarrow b$ satisfyingThus, for fixed $a$, the map $x\mapsto x\wedge a$ is left adjoint to $y\mapsto a\Rightarrow y$. A left adjoint preserves joins, soThis is one distributive law for lattices; the other follows from it and the absorption laws. Hence every Heyting algebra is a distributive lattice. This argument is the distributivity of a Heyting algebra.

Both sequents follow directly from the introduction and elimination rules of the implication-free fragment of intuitionistic propositional logic. From a proof of $\varphi \wedge (\psi \vee \chi )$, eliminate the conjunction to obtain $\varphi$ and $\psi \vee \chi$. Eliminate the disjunction: in the $\psi$ branch introduce $\varphi \wedge \psi$ and then the left disjunct; in the $\chi$ branch introduce $\varphi \wedge \chi$ and then the right disjunct. This yieldsConversely, eliminate the outer disjunction. From $\varphi \wedge \psi$, obtain $\varphi$ and introduce the left side of $\psi \vee \chi$; from $\varphi \wedge \chi$, obtain $\varphi$ and introduce its right side. In either branch, conjunction introduction produces $\varphi \wedge (\psi \vee \chi )$. HenceThis is the proof-theoretic form of the distributive law for lattices.