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?
 A: 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.)
A: 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.
