real numbers in the introduction

[mikeshulman]

Another one from James Hanson:

In set-theoretic foundations, the definition of the real numbers as equivalence classes of
Cauchy sequences requires either the law of excluded middle or the axiom of (countable)
choice to be well-behaved. But with higher inductive types, we can give a version of this
definition which is well-behaved and avoids any choice principles.

Now that we know that The HoTT reals coincide with the Escardó-Simpson reals, it follows that an equivalent construction to the HIIT reals could be done in impredicative constructive set theory by taking the Cauchy closure of the rationals inside the Dedekind reals. So while the statement is, strictly speaking, true, it may give a misleading impression of what is possible in set theory vs. in HoTT. I'm not sure how best to remedy this, especially since it depends on impredicativity, while predicativity hasn't been mentioned yet. Perhaps a footnote?

The Escardo-Simpson or higher inductive-inductive Cauchy reals could be done in predicative constructive set theory by adding an axiom and possibly any relevant signatures to the set theory which says that there is an initial Cauchy structure as defined by Booij, translating the relevant notions to first-order logic (i.e. contractible -> there exists a unique element, etc).

I don't see this as any different from the predicative constructivists who add an initial sigma-frame (which is a HIIT in HoTT) to their predicative constructive set theory to work with Dedekind-style reals.

[martinescardo]

As a side note, my former PhD student @abooij tried to publish this, but it was not deemed to be deep enough and worthy of publication by the referees. Perhaps you should try again, @abooij .

Another one from James Hanson:

In set-theoretic foundations, the definition of the real numbers as equivalence classes of
Cauchy sequences requires either the law of excluded middle or the axiom of (countable)
choice to be well-behaved. But with higher inductive types, we can give a version of this
definition which is well-behaved and avoids any choice principles.

Now that we know that The HoTT reals coincide with the Escardó-Simpson reals, it follows that an equivalent construction to the HIIT reals could be done in impredicative constructive set theory by taking the Cauchy closure of the rationals inside the Dedekind reals. So while the statement is, strictly speaking, true, it may give a misleading impression of what is possible in set theory vs. in HoTT. I'm not sure how best to remedy this, especially since it depends on impredicativity, while predicativity hasn't been mentioned yet. Perhaps a footnote?

[martinescardo]

As I see things, most HoTT/UF practicioners, and also the HoTT book, try to be predicative. Of course, an exception is the UniMath project. Moreover, the correspondence of HoTT/UF with ∞-toposes relies fundamentally on impredicativity. So perhaps the HoTT book should explicitly say something about this? I have to say that, for myself, it took me a while to figure out what exactly was going on regarding (im)predicativity in HoTT/UF.

[mikeshulman]

(Im)predicativity, in the sense relevant here (i.e. propositional resizing), is mentioned in section 3.5. I just meant it hadn't been mentioned yet in the introduction, which is where this comment occurs.

In set-theoretic foundations, the definition of the real numbers as equivalence classes of Cauchy sequences requires either the law of excluded middle or the axiom of (countable) choice to be well-behaved.

Also, this isn't true, either in set theory or in type theory. On one hand, one can use weaker choice principles like analytic LPO or just outright stipulate that the Dedekind and Cauchy reals coincide. On the other hand, even with countable choice there are issues with topology and pointwise analysis where one needs to also add the fan theorem.

But with higher inductive types, we can give a version of this definition which is well-behaved and avoids any choice principles.

What does well-behaved mean in this context? You can't use the higher inductive-inductive Cauchy reals in the real cohesion axiom since it doesn't have the same topology as the Dedekind reals, you have to use the Dedekind reals instead. In this sense, the Cauchy reals constructed in chapter 11 as a higher inductive-inductive type aren't well-behaved, and one has to use Cauchy nets or Cauchy filters if one wants a well-behaved type of reals.

Then there are the locale theorists who would argue that one should be using the locale of real numbers instead of the Cauchy, Escardo-Simpson, or Dedekind reals since the space of points isn't well behaved constructively compared to locales.

In set-theoretic foundations, the definition of the real numbers as equivalence classes of Cauchy sequences requires either the law of excluded middle or the axiom of (countable) choice to be well-behaved.

Also, this isn't true, either in set theory or in type theory. On one hand, one can use weaker choice principles like analytic LPO or just outright stipulate that the Dedekind and Cauchy reals coincide. On the other hand, even with countable choice there are issues with topology and pointwise analysis where one needs to also add the fan theorem.

The usual LPO for natural numbers should suffice here, even predicatively. The HoTT book only assumes that $\Omega$ is a sigma-frame when constructing the Dedekind real numbers. LPO implies that the booleans form a sigma-frame and can be used to define the Dedekind real numbers. LPO also implies that the resulting Dedekind real numbers has decidable strict order, since the existential quantifier used to define the strict order is decidable by LPO. Thus, said Dedekind real numbers coincide with the Cauchy real numbers via the proof in corollary 11.4.3.

[martinescardo]

Countable choice does suffice.