Homotopy Type Theory sigma-frame > history (changes)

Skip the Navigation Links | Home Page | All Pages | Latest Revisions | Authors |

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

Contents

< sigma-frame

category: redirected to nlab

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:
∀a∈L.∀s∈L ℕ.a∧⋁ n:ℕs(n)=⋁ n:ℕa∧s(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:ℕ→L⊢a∧⋁ n:ℕs(n)=⋁ n:ℕa∧s(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

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

EditDiscussPrevious revisionHide changesHistory (6 revisions) Print Source