The approximate Brouwer Fixed Point Theorem (aBFPT) for the standard $n$-simplex is:
Let $f$ be a uniformly continuous function from $\Delta^n$ into itself. Then for each $\varepsilon>0$ there exists $x\in\Delta^n$ such that $d(f(x),x)<\varepsilon$.
Does anyone know a reference for a full proof of aBFPT via Sperner's Lemma in Bishop-style constructive mathematics (BISH)?
If you don't know a reference but have a proof handy I'd very much like to see that as well.
Thank you in advance!
Note: The status of BFPT in constructive mathematics has been discussed in this MO post. For quick orientation: aBFPT may be viewed as constituting the constructive core of the full classical BFPT. The latter implies LLPO and is thus inherently nonconstructive (indeed, the two are equivalent over BISH since both are equivalent to WKL in the presence of countable choice). Classically, BFPT can be retrieved from aBFPT by a simple application of the Bolzano-Weierstrass theorem, which is equivalent to LPO over BISH and thus constructively inadmissible.