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

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

Contents

< sigma-complete lattice

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,,,,,)(L, \leq, \bot, \vee, \top, \wedge) with a function

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

such that denumerable/countable joins exist in the lattice:

n.sL .s(n) n:s(n)\forall n \in \mathbb{N}. \forall s \in L^\mathbb{N}. s(n) \leq \Vee_{n:\mathbb{N}} s(n)
xL.sL .(n.(s(n)x))( n:s(n)x)\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,,,,,)(L, \leq, \bot, \vee, \top, \wedge) with

  • a function

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

    n:,s:Li(n,s):s(n) n:s(n)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:Li(s,x):( n:(s(n)x))( n:s(n)x)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

References

Revision on June 10, 2022 at 11:26:55 by Anonymous?. See the history of this page for a list of all contributions to it.