## 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)$$ ## See also ## * [[integers]] * [[rational numbers]] * [[Archimedean ordered integral domain]]