Homotopy Type Theory decimal numeral representations of the natural numbers > history (Rev #2, changes)

Showing changes from revision #1 to #2: Added | Removed | Changed

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 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

  • natural numbers
  • infinite decimal representation of the sequential Cauchy real numbers?

Revision on February 27, 2022 at 08:04:42 by Anonymous?. See the history of this page for a list of all contributions to it.