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

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

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

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)