#Contents# * table of contents {:toc} Whenever editing is allowed on the [[nLab:HomePage|nLab]] again, this article should be ported over there. ## Definition ## ### In set theory ### 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) \}$$ ### In homotopy type theory ### 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)$$ ## See also ## * [[integers]] * [[rational numbers]] * [[Archimedean ordered integral domain]]