Homotopy Type Theory sigma-frame > history (Rev #2)

Contents

Definition

A σ\sigma-frame is a $\sigma$-complete lattice (L,,,,,,)(L, \leq, \bot, \vee, \top, \wedge, \Vee) with a family of dependent terms

a:L,s:La n:s(n)= n:as(n)a:L, s:\mathbb{N} \to L \vdash a \wedge \Vee_{n:\mathbb{N}} s(n) = \Vee_{n:\mathbb{N}} a \wedge s(n)

representing the countably infinitary distributive property for the lattice.

Examples

  • Sierpinski space, denoted as Σ\Sigma or 1 1_\bot, is the initial σ\sigma-frame.

See also

References

Revision on March 10, 2022 at 21:03:12 by Anonymous?. See the history of this page for a list of all contributions to it.