[[!redirects countably cocomplete (0,1)-category]] #Contents# * table of contents {:toc} ## Definition ## A __$\omega$-complete poset__ or __countably cocomplete (0,1)-category__ is a [[poset]] $(P, \leq)$ with * a term $\bot:P$ * a family of dependent terms $$a:P \vdash t(a):\bot \leq a$$ representing that $\bot$ is initial in the poset. * a function $$\Vee_{n:\mathbb{N}} (-)(n): (\mathbb{N} \to P) \to L$$ * a family of dependent terms $$n:\mathbb{N}, s:\mathbb{N} \to P \vdash i(n, s):s(n) \leq \Vee_{n:\mathbb{N}} s(n)$$ * a family of dependent terms $$x:\Sigma, s:\mathbb{N} \to \Sigma \vdash i(s, x):\left(\prod_{n:\mathbb{N}}(s(n) \leq x)\right) \to \left(\Vee_{n:\mathbb{N}} s(n) \leq x\right)$$ representing that denumerable/countable joins exist in the poset. ## See also ## * [[poset]] * [[join-semilattice]] * [[sigma-complete lattice]] * [[partial function classifier]] ## References ## * Partiality, Revisited: The Partiality Monad as a Quotient Inductive-Inductive Type ([abs:1610.09254](https://arxiv.org/abs/1610.09254))