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