Homotopy Type Theory irrational numbers > history (Rev #3, changes)

Showing changes from revision #2 to #3: Added | ~~Removed~~ | ~~Chan~~ged

Definition
- In set theory
- In homotopy type theory
See also

Whenever editing is allowed on the nLab again, this article should be ported over there.

Definition

Let $R$ be an Archimedean ordered integral domain with the integers $\mathbb{Z} \subseteq R$ being a integral subdomain of $R$ , with monic function $f:\mathbb{Z} \to R$ . The tight apartness relation $r # s$ in $R$ is defined as

In set theory

~~$r # s \coloneqq (r \lt s) \times (s \lt r)$~~

Let $R$ be an Archimedean ordered integral domain with the integers $\mathbb{Z} \subseteq R$ being a integral subdomain of $R$ , with injection $f \in R^\mathbb{Z} \to R$ . An element $r \in R$ is irrational if

~~Let us define the dependent type on $R$~~

isIrrational(r) \coloneqq \forall a \in \mathbb{Z}. \forall b \in \mathbb{Z}. ((f(a) \lt 0) \vee (0 \lt f(a))) \wedge ((f(a) \cdot r \lt f(b)) \vee (f(b) \lt f(a) \cdot r))

~~$isIrrational(r) \coloneqq \prod_{a:\mathbb{Z}} \prod_{b:\mathbb{Z}} (f(a) # 0) \times (f(a) \cdot r # f(b))$~~

The type of irrational numbers in $R$ is defined as

~~$r$ is irrational if the type $isIrrational(r)$ has a term.~~

Irrational(R) \coloneqq \{r \in R \vert isIrrational(r) \}

~~The type of irrational numbers in $R$ is defined as:~~

In homotopy type theory

~~$Irrational(R) \coloneqq \sum_{r:R} isIrrational(r)$~~

r # s \coloneqq \Vert (r \lt s) + (s \lt r) \Vert

Let us define the dependent type on $R$

isIrrational(r) \coloneqq \prod_{a:\mathbb{Z}} \prod_{b:\mathbb{Z}} (f(a) # 0) \times (f(a) \cdot r # f(b))

$r$ is irrational if the type $isIrrational(r)$ has a term.

The type of irrational numbers in $R$ is defined as:

Irrational(R) \coloneqq \sum_{r:R} isIrrational(r)

Homotopy Type Theory irrational numbers > history (Rev #3, changes)

Contents

Definition

In set theory

In homotopy type theory

See also