Is it possible to completely embed complete Heyting Algebras into upsets of a poset? Let $H$ be a Heyting algebra. It is a well-known result that there is a partially ordered set (Kripke frame) X such that there is an embedding of Heyting algebras $f: H \to \mathsf{Up}(X)$, where $\mathsf{Up}(X)$ consists of the up-sets of $X$. Specifically, take $X$ to consist of the prime filters of $H$, ordered by inclusion, and let $f(a) := \{ P \in X | a \in P \}$.
Is it possible to modify the result like this: Let $H$ be a complete Heyting algebra. Does there exists a complete embedding $g: H \to \mathsf{Up}(X)$ for some partially ordered set $X$? By a complete embedding, I mean an embedding preserving arbitrary meets and joins.
The approach above does not seem to work as it might be the case that there are incomplete prime filters on the complete Heyting algebra.
 A: Emil Jeřábek gave more complete answer than mine, so I have initially deleted it. On the afterthought, I decided to turn it into an addendum to Emil's answer. It is a generalization of sorts: if an embedding of a complete Heyting algebra $H$ into a co-Heyting algebra preserves finite joins and arbitrary meets (not necessarily infinite joins or implication), then $H$ itself is co-Heyting.
Indeed given such an embedding $i$, any $a\in H$ and any $S\subseteq H$ will satisfy
$$
i(a\lor\bigwedge S)=i(a)\lor i(\bigwedge S)=i(a)\lor\bigwedge i(S)=\bigwedge(i(a)\lor i(S))=\bigwedge i(a\lor S)=i(\bigwedge(a\lor S)),
$$
hence $a\lor\bigwedge S=\bigwedge(a\lor S)$.
Thus in particular if $H$ is not co-Heyting (and, for example, algebras of open sets of topological spaces usually are not), then any embedding of $H$ into any $\mathsf{Up}(X)$ fails to preserve some meet.
A: Let me give yet another characterization of these kind of complete Heyting algebras. Although the proof is more involved and set-theoretic in nature, I think the approach is worth since the equivalence is expressed in terms of a distributivity property of the complete Heyting algebra that coincides with complete distributivity in case it is Boolean. It follows, in particular, that any complete Boolean algebra that is not completely distributive (i.e., any Boolean algebra that is not a powerset) is a counterexample.

Proposition Let $H$ be a complete Heyting algebra. The following are equivalent:
1. H has a complete embedding into Up$(X)$ for some poset $X$.
2. Given a tree of arbitrary height $\gamma$ whose nodes are elements of $H$ such that:
$\bullet$ every node is the join of its immediate successors in the tree,
$\bullet$ every node at a limit level is the meet of its predecessors in the tree,
then whenever a set of nodes $S$ intersects every branch of the tree, the root $r$ is the join $\bigvee_{c \in S}c$.

Property 2 has been considered in my paper "Infinitary first-order categorical logic" (to appear in the Annals of Pure and Applied Logic) under the name transfinite transitivity (since it can be generalized to a similar property for Grothendieck topologies). It can be seen to imply that $H$ is completely distributive (hence co-Heyting) and in the Boolean case it is precisely equivalent to it, but it is in general strictly stronger than that (as the counterexample of the interval $([0, 1], \leq)$  shows). One way to see the equivalence is via the condition $3$ in Emil's answer.
Proof sketch
Emil's $3$ implies 2. Write the root of the tree as the join of the completely join-irreducible elements below it. Any of these must be below one immediate successor $a$, and hence below one immediate successor of $a$, and so on. One can then define by transfinite recursion a branch of the tree any of whose nodes is above that completely join-irreducible. Since the choice of this latter is arbitrary, we are done.
2. implies Emil's $3$. Let $\delta$ be the cardinality of $H$, and let $\kappa=(2^{\delta})^+$. Consider the canonical well-ordering $f: \kappa \times \kappa \to \kappa$; it has the property $f(\beta, \gamma) \geq \gamma$. For each $a \in H$ let $\mathcal{C}(a)$ be the set of tuples $(b_\alpha)_{\alpha<\lambda}$ of elements of $H$ such that $a = \bigvee_{\alpha<\lambda}b_{\alpha}$. Assume without loss of generality that $\mathcal{C}(a)$ is well-ordered and has order type $\kappa$ (repeating tuples, if needed). Let $a \in H$ be fixed. Then we can build a tree of height $\kappa$ whose nodes are elements of $H$, and having $a$ as a root, by transfinite recursion as follows. Assuming that the tree is defined for all levels $\lambda<\mu$; we show how to define the nodes of level $\mu$. If $\mu$ is a successor ordinal $\mu=\alpha+1$, and $\alpha=f(\beta, \gamma)$, by hypothesis the nodes $\{p_i\}_{i<m_{\gamma}}$ at level $\gamma$ are defined. To define the nodes at level $\alpha+1$, we need to define the successors of a node $n$ there; for this purpose, take then the $\beta-th$ tuple $(b_\alpha)_{\alpha<\nu} \in \mathcal{C}(p)$ over the predecessor $p$ of $n$ at level $\gamma$, and define the successors of $n$ to be $(n \wedge b_\alpha)_{\alpha<\nu}$. If $\mu$ is a limit ordinal, then define every node at level $\mu$ to be the meet of its predecessors.
Since the nodes on each branch $b$ decrease and $\kappa>\delta$, it stabilises at some node $c_b$. By construction, this $c_b$ is completely join-irreducible. Indeed, if $c_b=\bigvee_{\alpha<\nu}d_{\alpha}$, at some point of the recursion the successor of $c_b$ at some level will be $c_b \wedge d_{\alpha}$ for some $\alpha<\nu$, which implies that $c_b \leq d_{\alpha}$.
Finally, by 2., $a$ is the join $\bigvee_{b}c_b$, as we wanted to prove.
A: No, not in general: for instance, the real interval $([0,1],{\le})$, or any non-atomic complete Boolean algebra, do not have such an embedding. This follows from the following characterization:

Proposition: Let $H$ be a complete Heyting algebra. The following are equivalent:

*

*$H$ has a complete embedding into $\mathrm{Up}(X)$ for some poset $X$.


*$H$ is isomorphic to $\mathrm{Up}(X)$ for some poset $X$.


*Every element of $H$ is a join of a set of completely join-irreducible elements in $H$.

Proof sketch:
$2\to1$ is trivial.
$3\to2$: Let $X$ be the set of all completely join-irreducible elements of $H$, ordered upside down. Then the mapping $g\colon H\to\mathrm{Up}(X)$ given by
$$g(a)=\{x\in X:x\le a\}$$
is easily checked to be an isomorphism.
$1\to3$: Let $g\colon H\to\mathrm{Up}(X)$ be a complete embedding. For any $x\in X$, the set
$$P_x=\{a\in H:x\in g(a)\}$$
is a filter closed under arbitrary meets, i.e., principal: $P_x=[h(x),1]$ for some $h(x)\in H$. Moreover, $P_x$ is completely prime, hence the element $h(x)$ is completely join-irreducible.
Now, if $a,b\in H$ are such that $a\nleq b$, then there exists a completely join-irreducible element such that $u\le a$, and $u\nleq b$: indeed, $g(a)\nsubseteq g(b)$ as $g$ is an embedding, hence there is $x\in g(a)\smallsetminus g(b)$, and then $u=h(x)$ works.
This implies that any $a\in H$ is the join of all completely join-irreducible elements below it.
