< [[nlab:decimal rational number]] #Contents# * table of contents {:toc} ## Idea ## The decimal numbers as familiar from school mathematics. ## Definition ## The type of **decimal numbers**, denoted $\mathbb{Z}[1/10]$, is defined as the [[higher inductive type]] generated by: * A function $(-)/10^{(-)}:\mathbb{Z} \times \mathbb{N} \rightarrow \mathbb{Z}[1/10]$. The integer $a:\mathbb{Z}$ represents the integer if one ignores the decimal separator in the decimal numeral representation of the decimal number, and the natural number $b:\mathbb{N}$ represents the number of digits to the left of the final digit where the decimal separator ought to be placed after in the decimal numeral representation of the decimal number. * A dependent product of functions between identities representing that equivalent decimals are equal: $$equivdec : \prod_{a:\mathbb{Z}} \prod_{b:\mathbb{N}} \prod_{c:\mathbb{Z}} \prod_{d:\mathbb{N}} (a \cdot 10^d = c \cdot 10^b) \to (a/10^b = c/10^d)$$ (i.e. 1.00 = 1.000 with decimal numeral representations) * A set-truncator $$\tau_0: \prod_{a:\mathbb{Z}[1/10]} \prod_{b:\mathbb{Z}[1/10]} isProp(a=b)$$ ## See also ## * [[higher inductive type]] * [[natural numbers]] * [[integers]] * [[rational numbers]] * [[real numbers]]