Generating the Rationals
An inductive definition of the positive rational numbers
3 min,
490 words
Arnon Avron, who supervised my master's degree, once told me about a surprising little result that he had discovered. Paraphrasing:
Theorem. The positive rationals are freely generated by , where and .
If someone asked me why we need quotients to do math, rational numbers would probably be the first example I give. So it is interesting that the positive rationals can be given as an inductive type.
I don't know how Arnon proved it, but here is my take on it.