A dependent product of functions between identities representing that equivalent decimals are equal:
A set-truncator
Properties
TODO: Show that the decimal numbers are a Heyting ordered Heyting integral domain with decidable equality, decidable apartness, and decidable linear order, and that the decimal numbers are an a Heyting integral subdomain of the rational numbers.