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

Showing changes from revision #1 to #2: 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)

representing that denumerable/countable joins exist in the lattice.

See also

References

Revision on March 11, 2022 at 02:02:57 by Anonymous?. See the history of this page for a list of all contributions to it.