Homotopy Type Theory decimal numbers > history (Rev #9, changes)

Showing changes from revision #8 to #9: Added | Removed | Changed

Contents

Idea

The decimal numbers as familiar from school mathematics.

Definition

The type of decimal numbers, denoted [1/10]\mathbb{Z}[1/10], is defined as the higher inductive type generated by:

  • A function ()/10 ():×[1/10](-)/10^{(-)}:\mathbb{Z} \times \mathbb{N} \rightarrow \mathbb{Z}[1/10]. The integer a:a:\mathbb{Z} represents the integer if one ignores the decimal separator in the decimal numeral representation of the decimal number, and the natural number b:b:\mathbb{N} represents the number of digits to the left of the final digit where the decimal separator ought to be placed after in the decimal numeral representation of the decimal number.
  • A dependent product of functions between identities representing that equivalent decimals are equal:
    equivdec: a: b: c: d:(a10 d=c10 b)(a/10 b=c/10 d)equivdec : \prod_{a:\mathbb{Z}} \prod_{b:\mathbb{N}} \prod_{c:\mathbb{Z}} \prod_{d:\mathbb{N}} (a \cdot 10^d = c \cdot 10^b) \to (a/10^b = c/10^d)

    (i.e. 1.00 = 1.000 with decimal numeral representations)

  • A set-truncator
    τ 0: a:[1/10] b:[1/10]isProp(a=b)\tau_0: \prod_{a:\mathbb{Z}[1/10]} \prod_{b:\mathbb{Z}[1/10]} isProp(a=b)

See also

Revision on June 14, 2022 at 02:32:47 by Anonymous?. See the history of this page for a list of all contributions to it.