Homotopy Type Theory
omegacomplete poset > history (Rev #1)
Contents
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
References
 Partiality, Revisited: The Partiality Monad as a Quotient InductiveInductive Type (abs:1610.09254)
Revision on March 12, 2022 at 05:51:38 by
Anonymous?.
See the history of this page for a list of all contributions to it.