Rational Numbers [00ES]

We assume some construction of type of rational numbers. We assume that this type is a set with decidable equality, equipped with the usual addition and multiplication making it a field. We denote the field of rational numbers with . For a sketched construction see the HoTT book, section 11., section 11.1.

TODO: Make very clear what for what properties we need witnesses and find a construction we can borrow.