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 integral domain with decidable equality, decidable apartness, and decidable linear order, and that the decimal numbers are an integral subdomain of the rational numbers.