Showing changes from revision #20 to #21:
Added | Removed | Changed
The rational numbers as familiar from school mathematics.
The type of rational numbers, denoted , is 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.