## Real numbers ## ### Lattices and $\sigma$-frames ### A lattice is a [[set]] $L$ with terms $\bot:L$, $\top:L$ and functions $\wedge:L$, $\vee:L$, such that * $(L, \top, \wedge)$ and $(L, \bot, \vee)$ are [[commutative monoid]]s * $\wedge$ and $\vee$ are idempotent: for all terms $a:L$, $a \wedge a = a$ and $a \vee a = a$ * for all $a:L$ and $b:L$, $a \wedge (a \vee b) = a$ and $a \vee (a \wedge b) = a$ A $\sigma$-complete lattice is a lattice $L$ with a function $$\Vee_{n:\mathbb{N}} (-)(n): (\mathbb{N} \to L) \to L$$ such that * for all $n:\mathbb{N}$ and $s:\mathbb{N} \to L$, $$s(n) \wedge \left(\Vee_{n:\mathbb{N}} s(n)\right) = s(n)$$ * for all $x:L$ and $s:\mathbb{N} \to L$, if $s(n) \wedge x = s(n)$ for all $n:\mathbb{N}$, then $$\left(\left(\Vee_{n:\mathbb{N}} s(n)\right) \wedge x = \Vee_{n:\mathbb{N}} s(n)\right)$$ A $\sigma$-frame is a $\sigma$-complete lattice such that * for all $x:L$ and $s:\mathbb{N} \to L$, there exists a unique sequence $t:\mathbb{N} \to L$ such that for all $n:\mathbb{N}$, $t(n) = x \wedge s(n)$ and $$x \wedge \left(\Vee_{n:\mathbb{N}} s(n)\right) = \Vee_{n:\mathbb{N}} (t)$$ ### Sierpinski space ### Sierpinski space $\Sigma$ is an initial $\sigma$-frame, and thus could be generated as a [[higher inductive type]].