Homotopy Type Theory Sandbox (Rev #33, changes)

Showing changes from revision #32 to #33: Added | Removed | Changed

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 monoids

• $\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

such that

• for all $n:\mathbb{N}$ and $s:\mathbb{N} \to L$,

• for all $x:L$ and $s:\mathbb{N} \to L$, if $s(n) \wedge x = s(n)$ for all $n:\mathbb{N}$, then

A $\sigma$-frame is a $\sigma$ -complete lattice such with that a function$\mathcal{t}:(L \times (\mathbb{N} \to L)) \to \mathbb{N} \to L$ such that

• for all$x:L$

  for all $x:L$ and $s:\mathbb{N} \to L$, $\mathcal{t}(x,s)(n) = x \wedge s(n)$

  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

• for all $x:L$ and $s:\mathbb{N} \to L$,

Sierpinski space

Sierpinski space $\Sigma$ is an initial $\sigma$-frame, and thus could be generated as a higher inductive type.