The decimal numeral representations of the natural numbers as familiar from school mathematics.
Let the type of decimal digits, which we shall denote as , be the type inductively generated by the terms , , , , , , , , ,
The type of decimal numeral representations of the natural numbers, which we shall denote as , is a higher inductive type generated by:
A term representing the empty string of digits
A function: representing concatenation of a digit and a string of digits.
A dependent product of identities
representing that adding 0 to the left of any string of digits does not change the underlying value of the decimal numeral representation.
TODO: Define a successor function and show that is equivalent to the natural numbers. Then prove the addition and long multiplication algorithms for decimal numeral representations.