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

Author: mikeshulman

reals.tex

@@ -749,7 +749,7 @@ \subsection{Construction of Cauchy reals}
 Of course, our Cauchy approximations will now consist of Cauchy reals, rather than Dedekind reals or rational numbers.
 
 \begin{defn}\label{defn:cauchy-reals}
-  Let $\RC$ and the relation $\closesym:\Qp \times \RC \times \RC \to \type$ be the following higher inductive-inductive type family.
+  Let $\RC$ and the relation $\closesym:\RC \times \RC \times \Qp \to \type$ be the following higher inductive-inductive type family.
   The type $\RC$ of \define{Cauchy reals}
   \indexdef{real numbers!Cauchy}%
   \indexsee{Cauchy!real numbers}{real numbers, Cau\-chy}%