In 1978, in a series of unpublished conferences in Montréal, A. Joyal announced a remarkable theorem that unified several completeness theorems for fragments of first order logic, as well as first order logic itself. Given a coherent category $T$, we have the evaluation functor $e_T: T \to \mathcal{S}et^{\mathcal{M}od_c(T)}$, where $\mathcal{M}od_c(T)$ is the category of coherent models of $T$, and the evaluation functor sends an object $A$ to the set-valued functor from $\mathcal{M}od_c(T)$ that simply evaluates a model $M$ in $A$. The theorem is question is the following:
Theorem (Joyal): If $T$ is a Heyting category, then $e_T$ is a conservative Heyting functor.
The power and elegance of Joyal's formulation resides in the fact that it subsumes at least three different completeness theorems: that of coherent logic, that of classical first order logic, and, finally, that of intuitionistic first order logic. Indeed, the first follows from the conservativity of $e_T$, while the second is just the particular case when $T$ is a Boolean category (in which case coherent models are all Boolean). It is the third completeness theorem the most unexpected and amazing, and about which my question refers. The key fact here is that a Kripke model for an intuitionistic first order theory $T$ is the same thing as a Heyting functor $\mathcal{C}_T \to \mathcal{S}et^P$, where $P$ is the underlying poset of the model and $\mathcal{C}_T$ is the (Heyting) syntactic category of the theory. Now, the category $\mathcal{M}od_c(T)$ is not necessarily a poset (though it can be taken to be small), but Joyal's theorem provides us anyway with a generalized Kripke model which only differs in that aspect. In fact, the notion of forcing at a node $M$ coincides precisely with the satisfaction in the model $M$.
Now my question. In a paper by Makkai, the author mentions that "from the formulation of Joyal's theorem, it is quite easy to prove the existence of a conservative Heyting embedding of the form $e_T: T \to \mathcal{S}et^P$ with a poset $P$, with possible further conditions on $P$ (for example, regarding its size, or that it be a forest -a tree with many roots)". How exactly can this be achieved? The size is not an issue, since due to Löwenheim-Skolem theorem one can always cut down the category of models to restrict the cardinality. From the proof of Joyal's theorem, which can be found in Makkai-Reyes "First order categorical logic", I can also see that it is enough to consider only elementary embeddings as the morphisms in the category of models. Yet, this still doesn't necessarily make it into a poset. I also have an idea of which models can be taken as the roots of the forest, and how to derive a tree from a general poset with a bottom node, but cannot see how to bring the category of models into a posetal one. So, which is the argument Makkai is referring to?
EDIT
Andreas has given the right answer to the question. The non trivial thing in his construction of the poset $P$ is to prove that the functor $E^*: \mathcal{S}et^M \to \mathcal{S}et^P$ preserves $\forall$. Here is the calculation:
For a natural transformation $f: F \to G$ in $\mathcal{S}et^M$ and a subfunctor $A$ of $F$, we need to show that $E^*(\forall_fA)$ is the same subfunctor of $E^*(G)$ as $\forall_{E^*(f)}E^*(A)$. By definition, for any object $p$ in $P$ and $y \in E^*(G)(p)=G(E(p))$, we have $y \in \forall_{E^*(f)}E^*(A)(p)$ if and only if for all arrows $l: p \to q$ in $P$ one has:
$$E^*(f)_q^{-1}(G(E(l))(y)) \subseteq E^*(A)(q)$$
$$\iff (\forall x E^*(f)_q(x)=G(E(l))(y) \implies x \in E^*(A)(q))$$
$$\iff (\forall x f_{E(q)}(x)=G(E(l))(y) \implies x \in A(E(q))) (1)$$
On the other hand, also by definition, for $y \in G(E(p))$ one has $y \in \forall_fA(E(p))$ if and only if for all arrows $t: E(p) \to r$ in $M$ one has:
$$f_r^{-1}(G(t)(y)) \subseteq A(r)$$
$$\iff (\forall x f_r(x)=G(t)(y) \implies x \in A(r)) (2)$$
But because the functor $E$ is surjective (both on objects and arrows), we can find $q, l \in P$ such that $r=E(q)$ and $t=E(l)$, from which we deduce that $(1)$ and $(2)$ above are equivalent. Hence, $E^* \forall=\forall E^*$, as we wanted.
