nLab omega-complete poset

Contents

Context

(0,1)(0,1)-Category theory

Limits and colimits

Contents

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 is a poset (P,)(P, \leq) with

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

  • a function

    n:()(n):(P)L \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 nn \in \mathbb{N} and every sequence s:Ps \colon \mathbb{N} \to P we have

      s(n) n:s(n); s(n) \leq \Vee_{n \colon \mathbb{N}} s(n) \,;
    2. for every element aPa \in P and sequence s:Ps \colon \mathbb{N} \to P of elements a\leq a,

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

      we have

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

See also

References

  • Partiality, Revisited: The Partiality Monad as a Quotient Inductive-Inductive Type (arXiv:1610.09254)

Last revised on June 10, 2022 at 02:10:20. See the history of this page for a list of all contributions to it.