The ordering and lubs are, mutatis mutandis, as with the non-strict Construction [dt-002L].

The ordering and lubs are, mutatis mutandis, as with the non-strict Construction [dt-0021]. This operator is called a smash product because the two \bot values from A and B are "smashed" into one \bot value.

The ordering and lubs are, mutatis mutandis, as with the non-strict Construction [dt-0031]. This operator is called a smash sum because the two \bot values from A and B are "smashed" into one \bot value.

The strict cpo constructions satisfy all the usual isomorphisms, including:

• (A \mathbin {\circ \hspace{-0.4em}\twoheadrightarrow } B) \times (A \mathbin {\circ \hspace{-0.4em}\twoheadrightarrow } C)\;\; \simeq \;\; A \mathbin {\circ \hspace{-0.4em}\twoheadrightarrow } (B\otimes C)
• (A \otimes B \mathbin {\circ \hspace{-0.4em}\twoheadrightarrow } C) \;\; \simeq \;\; A \mathbin {\circ \hspace{-0.4em}\twoheadrightarrow } (B \mathbin {\circ \hspace{-0.4em}\twoheadrightarrow } C)
• (A \mathbin {\circ \hspace{-0.4em}\twoheadrightarrow } C) \times (B \mathbin {\circ \hspace{-0.4em}\twoheadrightarrow } C)\;\; \simeq \;\; (A\oplus B) \mathbin {\circ \hspace{-0.4em}\twoheadrightarrow } C

The category \mathbf {Cpo_\bot } is the category where the objects are cpos, the morphisms are strict continuous functions between these cpos, and composition and identity are as in \mathbf {Cpo}.

The lifting operator (\cdot )_\bot adds a new \bot value to a cpo. That is, for a cpo X: X_\bot = X \cup \{\bot \} \quad \text {(where $\bot \notin X$)} For all x \in X (including \bot _X), our new bottom value \bot \sqsubseteq x.

With the lifting operator, we can relate the lazy constructions like product and sum with strict constructions like smash product and sum via isomorphism:

• A\twoheadrightarrow B \simeq A_\bot \mathbin {\circ \hspace{-0.4em}\twoheadrightarrow } B
• A + B \simeq A_\bot \oplus B_\bot
• (A \times B)_\bot \simeq A_\bot \otimes B_\bot