Homotopy Type Theory decimal numeral representations of the natural numbers > history (changes)

Showing changes from revision #4 to #5: Added | Removed | Changed

Idea

< decimal numeral representation of the natural numbers

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 DD, be the type inductively generated by the terms 0:D0:D, 1:D1:D, 2:D2:D, 3:D3:D, 4:D4:D, 5:D5:D, 6:D6:D, 7:D7:D, 8:D8:D, 9:D9:D

The type of decimal numeral representations of the natural numbers, which we shall denote as N DN_D, is a higher inductive type generated by:

  • A term ϵ:N D\epsilon: N_D representing the empty string of digits

  • A function: ()():D×N DN D(-)(-): D \times N_D \to N_D representing concatenation of a digit and a string of digits.

  • A dependent product of identities

    ζ: a:N D0a=a\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 DN Ds:N_D \to N_D and show that (N D,ϵ,s)(N_D, \epsilon, s) is equivalent to the natural numbers. Then prove the addition and long multiplication algorithms for decimal numeral representations.

See also

Last revised on June 13, 2022 at 06:21:09. See the history of this page for a list of all contributions to it.