Homotopy Type Theory irrational numbers > history (Rev #1)

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 apartness relation $r # s$ in $\mathbb{Z}$ and $R$ is defined as

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

and the non-zero integers are defined as

\mathbb{Z}_{#0} \coloneqq \sum_{a:\mathbb{Z}} a # 0

with monic function $i:\mathbb{Z}_{#0} \to \mathbb{Z}$ .

Let us define the dependent type on $R$

isIrrational(r) \coloneqq \prod_{a:\mathbb{Z}_{#0}} \prod_{b:\mathbb{Z}} {f(i(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)