Homotopy Type Theory Sandbox (Rev #35, changes)

Showing changes from revision #34 to #35: Added | ~~Removed~~ | ~~Chan~~ged

On foundations

The natural numbers are characterized by their induction principle (in second-order logic/in a higher universe/as an inductive type). If one only has a first order theory, then one cannot have an induction principle, and instead one has a entire category of models. Thus, the first order models of arithmetic typically found in classical logic and model theory do not define the natural numbers, and this is true even of first-order Peano arithmetic.

Real Closed numbers rational interval arithmetic

~~Lattices and $\sigma$ -frames~~

The closed rational intervals are a subset of the product type $\mathbb{Q} \times \mathbb{Q}$ , defined as:

~~A lattice is a set $L$ with terms $\bot:L$ , $\top:L$ and functions $\wedge:L$ , $\vee:L$ , such that~~

\mathrm{ClosedIntervals}(\mathbb{Q}) \coloneqq \sum_{(a, b):\mathbb{Q} \times \mathbb{Q}} (a \leq b)

$(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$

The elements $[a, b]:\mathrm{ClosedIntervals}(\mathbb{Q})$ of the type are closed rational intervals.

~~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 with a function $\mathcal{t}:(L \times (\mathbb{N} \to L)) \to \mathbb{N} \to L$ such that~~

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

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

~~$x \wedge \left(\Vee_{n:\mathbb{N}} s(n)\right) = \Vee_{n:\mathbb{N}} t(x,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 11, 2022 at 18:52:24 by Anonymous?. See the history of this page for a list of all contributions to it.

Homotopy Type Theory Sandbox (Rev #35, changes)

On foundations

Real Closed numbers rational interval arithmetic

Lattices and σ\sigma-frames

Sierpinski space

Lattices and $\sigma$ -frames