Homotopy Type Theory sigma-frame > history (changes)

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

Contents

Whenever editing is allowed on the nLab again, this article should be ported over there.

Definition

In set theory

A $\sigma$-frame is a $\sigma$-complete lattice $(L, \leq, \bot, \vee, \top, \wedge, \Vee)$ such that the countably infinitary distributive property is satisfied:

$\forall a \in L. \forall s \in L^\mathbb{N}. a \wedge \Vee_{n:\mathbb{N}} s(n) = \Vee_{n:\mathbb{N}} a \wedge s(n)$

In homotopy type theory

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

$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_\bot$, is the initial $\sigma$-frame.

References

Last revised on June 10, 2022 at 15:24:28. See the history of this page for a list of all contributions to it.