make the types of ~_\epsilon consistent, close #1176

[mikeshulman]

No description provided.

[Bolpat]

The book uses $\sim\colon\mathbb Q_+\times\mathbb R_\mathsf c\times\mathbb R_\mathsf c\to\mathcal U$ in the beginning of Definition 11.3.2 as well as $\sim\colon\mathbb R_\mathsf c\to\mathbb R_\mathsf c\to\mathbb Q_+\to\mathcal U$ after the first set of bullet points. This PR wants to replace the first signature by the latter, which is good for consistency.

Personally, I prefer neither signature, but a mixture: Conceptually, $\sim$ is a function relation that maps $\epsilon\colon\mathbb Q_+$ to a binary relation of Cauchy reals $\mathbb R_\mathsf c\times\mathbb R_\mathsf c\to\mathcal U$. Whether we use $\mathbb R_\mathsf c\times\mathbb R_\mathsf c\to\mathcal U$ or $\mathbb R_\mathsf c\to\mathbb R_\mathsf c\to\mathcal U$ is probably quite irrelevant from a didactic standpoint, but I feel like

• $\mathbb Q_+$ should be first because the relation is used with Currying ― and
• the operator after $\mathbb Q_+$ should be $\to$ and not $\times$.

Then, in § 11.3.2, the type of $B$ should (probably) be:

$$B\colon\prod_{x,y\colon\mathbb R_\mathsf c}\prod_{\epsilon\colon\mathbb Q_+}x\sim_\epsilon y\to A(x)\to A(y)\to\mathcal U$$

and later in the text

$$B\colon\mathbb Q_+\to A\to A\to\mathcal U$$

and the application $B(x, y, a, b, ϵ, ξ)$ would have to be $B(ϵ, ξ, x, y, a, b)$. This again makes more sense because later, we define $\frown^ξ_ϵ$ which is conceptually a relation between pairs.
Then, in the discussion of the induction principle of Cauchy reals, the arguments to $g$ should be flipped:

$$g\colon\prod_{ϵ\colon\mathbb Q_+}\prod_{\xi\colon x\sim_ϵy}\prod_{x,y\colon\mathbb R_\mathsf c}\dots{}$$

Later, the application of $g$ must be changed as well: $g(x_ϵ,x_δ,ϵ+δ,ξ)$ should become $g(ϵ+δ,ξ,x_ϵ,x_δ)$.
Later, in the paragraph before Lemma 11.3.12, it probably makes sense to flip the quantifiers after “The resulting conclusion is”: $∀(u,v\colon\mathbb R_\mathsf c). ∀(ϵ\colon\mathbb Q_+)$ should be $∀(ϵ\colon\mathbb Q_+). ∀(u,v\colon \mathbb R_\mathsf c)$; this is minor, though. The same applies to formula (11.3.13).
In the proof of Lemma 11.3.15, in the definition of $\frown$, reorder the parameter types to $\mathbb Q_+\to\mathbb R_\mathsf c\to\mathbb R_\mathsf c\to\mathsf{Prop}$.

In Theorem 11.3.16, reorder the type of $\approx$. I don’t really understand the proof of the theorem, where it probably also applies, however, there it seems the particular ordering of parameter types is actually used.

I haven’t looked much further in the chapter.

[mikeshulman]

That's more or less what I meant in my comment on #1176 by "on general principles the first might be preferable", and if we were writing the book again from scratch maybe we ought to do it that way. But I don't know that it's worth trying to make such a big change now. In particular, since we have no typechecker to ensure that we catch all the occurrences, trying to make such a change might cause more confusion than it alleviates.