# Homotopy Type Theory sigma-complete lattice > history (changes)

Showing changes from revision #7 to #8: Added | Removed | Changed

# Contents

Whenever editing is allowed on the nLab again, this article should be ported over there.

## Definition

### In set theory

A $\sigma$-complete lattice is a lattice $(L, \leq, \bot, \vee, \top, \wedge)$ with a function

$\Vee_{n:\mathbb{N}} (-)(n): (\mathbb{N} \to L) \to L$

such that denumerable/countable joins exist in the lattice:

$\forall n \in \mathbb{N}. \forall s \in L^\mathbb{N}. s(n) \leq \Vee_{n:\mathbb{N}} s(n)$
$\forall x \in L. \forall s \in L^\mathbb{N}. (\forall n \in \mathbb{N}.(s(n) \leq x)) \implies \left(\Vee_{n:\mathbb{N}} s(n) \leq x\right)$

### In homotopy type theory

A $\sigma$-complete lattice is a lattice $(L, \leq, \bot, \vee, \top, \wedge)$ with

• a function

$\Vee_{n:\mathbb{N}} (-)(n): (\mathbb{N} \to L) \to L$
• a family of dependent terms

$n:\mathbb{N}, s:\mathbb{N} \to L \vdash i(n, s):s(n) \leq \Vee_{n:\mathbb{N}} s(n)$
• a family of dependent terms

$x:L, s:\mathbb{N} \to L \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 lattice.