Typo in the definition of Cauchy reals and Cauchy approximations.

[damhiya]

In the Definition 11.3.2 (Cauchy reals and Cauchy approximations), the relation ~ is given two different types ℚ₊ × ℝ × ℝ → U and ℝ → ℝ → ℚ₊ → U. ~_ε : ℝ → ℝ → Prop is also used in the text.

This can be represented by a family of binary relations, which we will denote ∼_e : ℝ → ℝ → Prop.

It would be better to unify the convention.

[mikeshulman]

Good catch. It seems that the second type is the more common one in the text, so probably we should switch to that one (although on general principles the first might be preferable). I'm not too bothered about the difference between U and Prop as the codomain, though, since we generally implicitly coerce propositions to types.

[damhiya]

Thank you!