The decimal numbers as familiar from school mathematics.
Definition
The type of decimal numbers, denoted , is defined as the higher inductive type generated by:
A function . The integer represents the integer if one ignores the decimal separator in the decimal numeral representation of the decimal number, and the natural number 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:
(i.e. 1.00 = 1.000 with decimal numeral representations)