# Defining rational numbers without using quotients or 0-truncations

Most definitions of the rational numbers as a higher inductive type in univalent homotopy type theory (such as those in the cubical Agda library for example) require either the use of a quotient set or a 0-truncation constructor. Is there a way to define the rational numbers as a higher inductive type without using either quotient sets or 0-truncation?

• Unless you impose other criteria, you can just take $\mathbb{Q} = \mathbb{N}$. You will suffer a bit when defining the arithmetical operations on $\mathbb{Q}$, but it is doable. So what other criteria would you like to impose (why do you dislike my proposed solution)? – Andrej Bauer Jun 24 at 19:58
• Neil Strickland's answer below says that one could construct the positive rationals as an inductive type with a term $1$ and two functions $x \mapsto x+1$ and $x \mapsto x/(x+1)$. The positive integers, which are isomorphic to the natural numbers, could also be defined as an inductive type with a term $1$ and two functions $x \mapsto 2x$ and $x \mapsto 2x+1$. In that case, one could take $\mathbb{Q}^+ = \mathbb{N}$, and $\mathbb{Q} = \mathbb{Q}^+ + 1 + \mathbb{Q}^+ = \mathbb{N} + 1 + \mathbb{N} = \mathbb{Z}$, which is very similar to your answer. – Madeleine Birchfield Jun 25 at 16:01

One version of the theory of continued fractions is as follows. We can define operations $$S,T,J\colon\mathbb{Q}^+\to\mathbb{Q}^+$$ by $$S(x)=x+1$$ and $$J(x)=1/x$$ and $$T(x)=JSJ(x)=x/(x+1)$$, then we can define $$M$$ to be the free monoid generated by $$S$$ and $$T$$. We then have an evaluation map $$M\to\mathbb{Q}^+$$ given by $$m\mapsto m(1)$$, and it is not hard to check that this is a bijection.

If we wanted, we could turn this around and essentially define $$\mathbb{Q}^+$$ to be the same as $$M$$ (and $$\mathbb{Q}$$ to be $$\{0\}\amalg\mathbb{Q}^+\amalg -\mathbb{Q}^+$$). This makes $$\mathbb{Q}$$ into an inductive type. The ordering on $$\mathbb{Q}$$ and the inclusion $$\mathbb{Z}\to\mathbb{Q}$$ work nicely in this picture, but the algebraic operations are awkward.

You can also introduce the type $$R$$ of $$2\times 2$$ matrices $$\begin{pmatrix} a&b\\c&d\end{pmatrix}$$ with $$a,c,d\in\mathbb{Z}^+$$ and $$b\in\mathbb{N}$$ and $$ad=bc+1$$. Given a positive rational $$q\in\mathbb{Q}^+$$ we can write it as $$q=a/c$$ with $$\text{gcd}(a,c)=1$$. This means that there exist $$b,d\in\mathbb{Z}$$ with $$ad=bc+1$$. We can change the pair $$(b,d)$$ by adding multiples of $$(a,c)$$, so there is choice with $$0. From this we get $$b=(ad-1)/c$$ with $$0 so $$0\leq b. This shows that the map $$\begin{pmatrix} a&b\\c&d\end{pmatrix}\mapsto a/c$$ gives a bijection $$R\to\mathbb{Q}^+$$, which is a version of Noah Snyder's answer. I think that this can be done in a fairly satisfactory way from the inductive definitions, and that one can use the interplay between $$\mathbb{Q}^+$$ and $$R$$ to define the algebraic operations on $$\mathbb{Q}^+$$. I have partially done this in Lean but I have not thought about it for a while and do not remember precisely what was the state of play.

You could try defining them as triples of an integer, a positive integer, and a proof that those two integers are relatively prime.

(It's conceivable that I've missed something technical here about whether proofs that pairs are relatively prime is already a $$(-1$$)-type without any truncation, but I think it should be ok.)

• Here's one example of how you need to be careful. It's tempting to define "relatively prime" to mean that ax+by=1 has a solution, but then you'd need to truncate or quotient, because there are many witnesses. – Noah Snyder Jun 24 at 17:28
• But it should work to define relatively prime as gcd(a,b)=1, right? – Mike Shulman Jun 24 at 17:50
• Yes, I think so, but was hoping you or someone else who thinks constructively more often would be more confident than me. – Noah Snyder Jun 24 at 18:00
• this is close to the definition of the rationals in the Agda standard library. – Noam Zeilberger Jun 24 at 18:23
• Anything decidable can be made into a proposition without truncation: 1 if it's true, or 0 if it's false. – James Wood Jun 25 at 8:33