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

Definition
- In set theory
- In homotopy type theory
Examples
See also
References

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

Alex Simpson, Measure, randomness and sublocales.
Univalent Foundations Project, Homotopy Type Theory – Univalent Foundations of Mathematics (2013)

Revision on June 9, 2022 at 09:05:21 by Anonymous?. See the history of this page for a list of all contributions to it.