## Idea ## The decimal numeral representations of the natural numbers as familiar from school mathematics. ## Definition ## Let the type of decimal digits, which we shall denote as $D$, be the type inductively generated by the terms $0:D$, $1:D$, $2:D$, $3:D$, $4:D$, $5:D$, $6:D$, $7:D$, $8:D$, $9:D$ The type of **decimal numeral representations of the natural numbers**, which we shall denote as $N_D$, is a [[higher inductive type]] generated by: * A term $\epsilon: N_D$ representing the empty string of digits * A function: $(-)(-): D \times N_D \to N_D$ representing concatenation of a digit and a string of digits. * A dependent product of identities $$\zeta: \prod_{a:N_D} 0a = a$$ representing that adding 0 to the left of any string of digits does not change the underlying value of the decimal numeral representation. ## Properties ## TODO: Define a successor function $s:N_D \to N_D$ and show that $(N_D, \epsilon, s)$ is equivalent to the natural numbers. Then prove the addition and long multiplication algorithms for decimal numeral representations. ## See also ## * [[natural numbers]]