Homotopy Type Theory Sandbox (Rev #32, changes)

Showing changes from revision #31 to #32: Added | ~~Removed~~ | ~~Chan~~ged

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

\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 \land (\underset{n : ℕ}{⋁} s (n)) = \underset{n : ℕ}{⋁} (x t \land s (n))

x \wedge \left(\Vee_{n:\mathbb{N}} s(n)\right) = \Vee_{n:\mathbb{N}} (x (t) ~~\wedge~~ ~~s(n))~~

Sierpinski space

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

Revision on May 8, 2022 at 17:28:39 by Anonymous?. See the history of this page for a list of all contributions to it.