Esakia duality

Statement

Let $f \colon X \to Y$ be a continuous order-preserving map between Esakia spaces. Call $f$ an Esakia morphism if for all $x \in X$ and $y \in Y$ with $f(x) \le y$ there is $z \in X$ with $x \le z$ and $f(z) = y$. Let $\mathbf{HA}$ be the category of Heyting algebras with homomorphisms that preserve $0$, $1$, $\wedge$, $\vee$ and $\to$. Let $\mathbf{Esa}$ be the category of Esakia spaces with Esakia morphisms. Then $\mathbf{HA}$ is dually equivalent to $\mathbf{Esa}$, that is, $\mathbf{HA}$ is equivalent to the opposite category of $\mathbf{Esa}$.

1. A Heyting algebra $H$ goes to the set $X_H$ of prime filters of $H$, ordered by inclusion. Its topology is generated by the sets $\set{P : a \in P}$ and $\set{P : a \notin P}$ for $a \in H$.
2. An Esakia space $X$ goes to the Heyting algebra of its clopen up-sets, with $U \to V = X \setminus {\downarrow}(U \setminus V)$.
3. The map $a \mapsto \set{P \in X_H : a \in P}$ is an isomorphism from $H$ onto the clopen up-sets of $X_H$.