The rational numbers as familiar from school mathematics.
The type of rational numbers, denoted , has several definitions as a higher inductive type.
The rational numbers are defined as the higher inductive type generated by:
and is the apartness relation on the integers.
where is the inclusion of the nonzero integers in the integers.
TODO: Show that the rational numbers are a Heyting ordered field with decidable equality, decidable apartness, and decidable linear order, and that the rational numbers are initial in the category of Heyting ordered fields. The HoTT book unfortunately skips the proof entirely.