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 0truncation constructor. Is there a way to define the rational numbers as a higher inductive type without using either quotient sets or 0truncation?

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
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=(ad1)/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.
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.)

$\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