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.