#Contents# * table of contents {:toc} Whenever editing is allowed on the [[nLab:HomePage|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. ## See also ## * [[lattice]] * [[sigma-frame]] * [[omega-complete poset]] ## References ## * Alex Simpson, [Measure, randomness and sublocales](https://www.sciencedirect.com/science/article/pii/S0168007211001874).