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

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 injection $f \in R^\mathbb{Z}$ . The tight apartness relation $r # s$ in $R$ is defined as

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

An element $r \in R$ is irrational if

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

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

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

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 \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)