6
$\begingroup$

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?

$\endgroup$
2
  • 3
    $\begingroup$ 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)? $\endgroup$ – Andrej Bauer Jun 24 at 19:58
  • 1
    $\begingroup$ 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. $\endgroup$ – Madeleine Birchfield Jun 25 at 16:01
12
$\begingroup$

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<d\leq c$. From this we get $b=(ad-1)/c$ with $0<ad\leq ac$ so $0\leq b<c$. 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.

$\endgroup$
9
$\begingroup$

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.)

$\endgroup$
5
  • $\begingroup$ 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. $\endgroup$ – Noah Snyder Jun 24 at 17:28
  • 1
    $\begingroup$ But it should work to define relatively prime as gcd(a,b)=1, right? $\endgroup$ – Mike Shulman Jun 24 at 17:50
  • $\begingroup$ Yes, I think so, but was hoping you or someone else who thinks constructively more often would be more confident than me. $\endgroup$ – Noah Snyder Jun 24 at 18:00
  • 3
    $\begingroup$ this is close to the definition of the rationals in the Agda standard library. $\endgroup$ – Noam Zeilberger Jun 24 at 18:23
  • $\begingroup$ Anything decidable can be made into a proposition without truncation: 1 if it's true, or 0 if it's false. $\endgroup$ – James Wood Jun 25 at 8:33

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.