In Johnstone's Stone Spaces it is proved that the category of profinite partial orders is (equivalent to) the category of ordered Stone spaces (also called Priestley spaces) and that the obvious embedding from finite partial orders into Priestley spaces is the pro-completion of finite partial orders.

Main question: Does it follow that there exists a profinite completion functor from partial orders to Priestley spaces?

If yes, is there an explicit construction of the profinite completion of a partial order?

For example, does anyone know what does the profinite completion of the partial order $(\omega,=)$ look like?

Moreover, profinite quasi-orders are the the Priestley quasi-orders, i.e. quasi-ordered Stone spaces such that if $x\not\leq y$ then there is a clopen downset $D$ such that $y\in D$ and $x\not\in D$. I have the same questions about the profinite completion of a quasi-order. In this context, does one gain anything by considering quasi-order instead of partial orders?

For the record I asked this question on MathSE, here.

My abstract try:

The category $\mathbf{Qo}$ of quasi-orders with monotone maps is complete. The inclusion of $\mathbf{Qo}_\text{fin}$, the finite quasi orders, into $\text{Pro-}\mathbf{Qo}_\text{fin}$ extends to the functor $U:\text{Pro-}\mathbf{Qo}_\text{fin}\to \mathbf{Qo}$, bringing a formal directed limit $\lim_i Q_i$ of finite qo's to the actual limit of this diagram in $\mathbf{Qo}$. Since $\text{Pro-}\mathbf{Qo}_\text{fin}$ is equivalent to $\mathbf{PrQo}$ the category of Priestley qos, if I am not mistaken, the above functor $U:\mathbf{PrQo}\to\mathbf{Qo}$ is simply the forgetful functor. The profinite completion functor $P:\mathbf{Qo}\to\mathbf{PrQO}$ would be the left adjoint of $U$. Can we use some adjoint functor theorem to conclude?

More pedestrian try:

Let $Q$ be a partial order and $\langle p_i:Q\to Q_i \rangle$ the cofiltered diagram of its finite po quotients. Let $P(Q)=\lim_i Q_i$ be the limit in the category of Priestley spaces, each $Q_i$ considered discrete of course, and $i_Q:Q\to P(Q)$ the natural monotone mapping.

Then for every montone map $g:P\to F$ for $F$ finite, there exists a unique Priestley map $\hat{g}:P(Q)\to F$ (namely, the corresponding projection) such that $\hat{g}\circ i_Q=g$. Now let $f:Q\to X$ be a monotone map into a Priestley space $X$. Then $X$ is the cofiltered limit of $\langle q_j:X\to X_j \rangle$ its finite quotients in the category of Priestley spaces. For every $j$ the map $q_j\circ f:Q\to X_j$ extends to a Priestley map $\widehat{q_j\circ f}:P(Q)\to X_j$. By the universal property of the limit $X=\lim_j X_j$ we get a Priestley map $\bar{f}:P(Q)\to X$ such that in the category of partial orders $\bar{f}\circ i_Q=f$.