# Homotopy Type Theory omega-complete poset > history (changes)

Showing changes from revision #1 to #2: Added | Removed | Changed

# 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.