Does the Category of CPOs have omega^op limits?

Question

In "Domains and Lambdi Calculi" by Amadio and Curien, in the section on solving recursive domain equations (section 7), they give sufficient conditions on a cpo-enriched category so that the category of embedding-projection pairs has $\omega$-colimits. Specifically they say it is sufficient for the category to have $\omega^{op}$-limits.

They then have a theorem that the category of CPOs has all $\omega^{op}$ limits, but the proof is incomplete and I don't see how it could be completed.

To be clear in their book the category CPO has as objects directed complete partial orders with a least element and as maps continuous (not neccesarily strict!) functions.

Their proof proceeds as follows. Given a diagram ${D_n,f_n}_{n\in\omega}$ ($f_n : D_{n+1} \to D_n)$, their proposed limit is $$D = \{ \alpha : \Pi_{n\in\omega} D_n | \forall n, f_n(\alpha_{n+1}) = \alpha_{n} \}$$

with the pointwise ordering. This is definitely the product of that diagram in DCPO, but I don't see why $D$ must have a least element. In particular, you can't pick $\alpha_n = \bot_n \in D_n$ since the functions $f_n$ are not assumed to be strict.

However, restricting to strict continuous functions is all they need anyway because embedding-projection pairs of CPOs are strict anyway (embedding because it's a left adjoint, projection because it's a retract of the embedding). However this doesn't seem quite right either because for example a right adjoint wouldn't necessarily have to be strict, so it seems less general.

So to summarize

1. Is there a way to prove $D$ is a CPO or a concrete counterexample?
2. If it's not, what is the right way to "fix" to their formula for solving recursive domain equations? Specifically, we do want to limit the construction to a category of CPOs since they have the bottom elements needed for recursive domain equations, but restricting to limits of strict functions seems stronger than necessary (though sufficient for my needs for now).

I know I could go back through Wand and Plotkin and Pitts and probably find the answers to (3) there, but it would be nice to have a succinct general construction like in their book chapter. Specifically I would like a reference that includes Pitt's minimal invariants work (otherwise Abramsky-Jung is probably sufficient).

Answer 1

Here's an attempt (please check!).

We have that $\bot_D = d$, where

$$ d_i = \bigsqcup^{D_i} \{\bot_i,f_i(\bot_{i+1}),f_i(f_{i+1}(\bot_{i+2})),\ldots\} $$

By construction (and monotonicity), the above is the supremum of an $\omega$-chain inside $D_i$, so $d_i$ is well defined.

It is an element of $D$ since, by continuity,

$$ \begin{array}{ll} & f_i(d_{i+1}) \\ = & f_i(\bigsqcup^{D_{i+1}} \{\bot_{i+1},f_{i+1}(\bot_{i+2}),f_{i+1}(f_{i+2}(\bot_{i+3})),\ldots\}) \\ = & \bigsqcup^{D_{i}} \{f_i(\bot_{i+1}),f_i(f_{i+1}(\bot_{i+2})),f_i(f_{i+1}(f_{i+2}(\bot_{i+3}))),\ldots\} \\ = & \bigsqcup^{D_{i}} \{\bot_i, f_i(\bot_{i+1}),f_i(f_{i+1}(\bot_{i+2})),f_i(f_{i+1}(f_{i+2}(\bot_{i+3}))),\ldots\} \\ = & d_i \end{array} $$

To prove that $d$ is the bottom, we take any $x \in D$, and we observe

$$ \begin{array}{ll} & d_i \sqsubseteq x_i \\ \Leftarrow & \forall k\geq i.\ f_i \circ \cdots \circ f_k(\bot_{k+1}) \sqsubseteq x_i \\ \Leftarrow & \forall k\geq i.\ f_i \circ \cdots \circ f_k(\bot_{k+1}) \sqsubseteq f_i \circ \cdots \circ f_k (x_{k+1})\\ \Leftarrow & \forall k\geq i.\ \bot_{k+1} \sqsubseteq x_{k+1}\\ \Leftarrow & {\sf true} \end{array} $$