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

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,,,,,,)(L, \leq, \bot, \vee, \top, \wedge, \Vee) such that the countably infinitary distributive property is satisfied:

aL.sL .a n:s(n)= n:as(n)\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,,,,,,)(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 April 14, 2022 at 02:45:37 by Anonymous?. See the history of this page for a list of all contributions to it.