added pointer to:

]]>just to highlight that we can’t just drop the HoTT book without commentary into generic entries – this gives a weird impression to the general reader of the nLab.

There needs to be at least a line like: “Discussion in homotopy type theory…” and then there should also a pointer to page and verse in the book. Like this:

]]>Discussion in homotopy type theory:

adding definition of rational numbers as a higher inductive type in homotopy type theory from the HoTT book.

Anonymous

]]>Are you asking for a reference on rational numbers?

In any case, the entry should indeed give some textbook references. For the moment I have added pointer to the Wikipedia article, which lists references.

]]>Might You, please, indicate any reference?

Thank You very much!

Carlo Perrone ]]>

every $\mathbb{Z}$-algebra is a ring.

Anonymous

]]>Redirect: rationals

]]>