nLab omega-complete poset

Idea

An $\omega$-complete poset, in the following sense, is a poset with countable joins, hence a countably cocomplete poset.

Definition

A $\omega$-complete poset or a $\omega$-cpo is a poset $(P, \leq)$ with

• an initial element $\bot \in P$ (bottom), hence such that for every element $a \in P$ we have $\bot \leq a$;

• a function

  $$\Vee_{n \colon \mathbb{N}} (-)(n) \;\colon\; (\mathbb{N} \to P) \to L$$

  exhibiting the existence of denumerable/countable joins in the poset, namely such that

  1. for every natural number $n \in \mathbb{N}$ and every sequence $s \colon \mathbb{N} \to P$ we have

     $$s(n) \leq \Vee_{n \colon \mathbb{N}} s(n) \,;$$

  2. for every element $a \in P$ and sequence $s \colon \mathbb{N} \to P$ of elements $\leq a$,

     $$\prod_{n \colon \mathbb{N}} (s(n) \leq a) \,,$$

     we have

     $$\Vee_{n \colon \mathbb{N}} s(n) \leq a \,.$$

See also

• poset

• join-semilattice

• sigma-complete lattice

• partial function classifier

• directed-complete poset

References

• Thorsten Altenkirch, Nils Anders Danielsson, Nicolai Kraus, Partiality, Revisited: The Partiality Monad as a Quotient Inductive-Inductive Type (abs:1610.09254)

• Martin E. Bidlingmaier, Florian Faissole, Bas Spitters, Synthetic topology in Homotopy Type Theory for probabilistic programming. Mathematical Structures in Computer Science, 2021;31(10):1301-1329. [doi:10.1017/S0960129521000165, arXiv:1912.07339]