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

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

Contents

Definition

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,n:,s:Li(n,s,x):(s(n)x)( n:s(n)x)x:L, n:\mathbb{N}, s:\mathbb{N} \to L \vdash i(n, s, x):(s(n) \leq x) \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 March 12, 2022 at 05:12:40 by Anonymous?. See the history of this page for a list of all contributions to it.