 and then, using the type-theoretic axiom of choice (see Section 4 below), find a function \(f : \bR\rightarrow \bZ\) such that \(f(x) \lt x \lt f(x)+2\). However, there is no reason to believe that the function \(f\) respects the equivalence relations—that is, that \(f(x) = f(y)\) holds if \(x \sim y\).