Brouwer's Fixed Point Theorem (BFPT) is not provable in Bishop-style constructive mathematics (BISH). For quick orientation, BISH is obtained from classical mathematics by removing the Law of Excluded Middle (LEM) and replacing the full Axiom of Choice by the Axiom of Dependent Choice.
Standard classical proofs of BFPT either rely on LEM or the Bolzano-Weierstrass Theorem, which is equivalent to the Limited Principle of Omniscience, a constructively inadmissible weakening of LEM. BFPT itself is equivalent to Weak König's Lemma in BISH, and thus to the Lesser Limited Principle of Omniscience, another constructively inadmissible weakening of LEM.
However, the following approximate version of BFPT is known to be provable in BISH.
Recall that $$\Delta^n=\bigg\{\textbf{x}=(x_0,...,x_n)\mid\sum_{i=0}^{n}x_i\leq1 \land \forall i: 0\leq x_i \leq 1 \bigg\}$$ and let $d$ be the Euclidian metric on $\Delta^n$.
Approximate Brouwer Fixed Point Theorem
Let $f$ be a uniformly continuous function from $\Delta^n$ into itself. Then for each $\varepsilon>0$ there exists $\textbf{x}\in\Delta^n$ such that $d(f(\textbf{x}),\textbf{x})<\varepsilon$.
The assumption of uniform continuity is essential since the classical Uniform Continuity Theorem is not provable in BISH. Here's my proof attempt:
The proof in BISH proceeds via Sperner's Lemma.
Consider a uniformly continuous function $f$ from $\Delta^n$ into itself. Fix $m,k\in\mathbb{N}$ such that $2^{-k}+2^{-k-2}+2^{-k-3}<2^{-m}$ and $$d(\textbf{x},\textbf{y})<2^{-k}+2^{-k-2}\Longrightarrow d(f(\textbf{x}),f(\textbf{y}))<2^{-m}.$$
Consider a simplical subdivision $\mathcal{S}$ of $\Delta^n$ with grid size $2^{-k}$. Specify a labeling as follows. A vertex $x$ of a simplex in $\mathcal{S}$ gets assigned the label $i$ if, and only if, $f(\textbf{x})_i<x_i$ or $f(\textbf{x})_i<x_i+2^{-k-3}$. This is constructively well-defined by the Approximate Splitting Principle and constitutes a feasible labeling in the sense of Sperner's Lemma. Thus, $\mathcal{S}$ contains a subsimplex $S$ whose $n+1$ vertices are labeled with $0,1,...,n$. We must now show that for a vertex $\textbf{s}$ of $S$, $d(f(\textbf{s}),\textbf{s})<n(2^{-m+1})$ holds (cf. Scarf, 1967; van Dalen, 2011).
This is where I got stuck.
Denote the vertex of $S$ labeled by $j$ by $\textbf{s}^j$ and consider $\textbf{s}^1$. By the definition of the labeling, $f(\textbf{s}^1)_1<s^1_1+2^{-k-3}$ and for each $i\neq 1$, we have $f(\textbf{s}^i)_i<s^i_i+2^{-k-3}$. I just can't figure out how to infer from this and the uniform continuity of $f$ that $d(f(\textbf{s}^1),\textbf{s}^1)<n(2^{-m+1})$ must hold.
I'm sure the argument is fairly easy, but I just can't see it. A "visual" argument for $\Delta^2$ is in the paper by van Dalen referenced above. While it helps me see that the conclusion is true for $\Delta^1$ and $\Delta^2$, I am still unable to derive it formally, let alone generalize it to $\Delta^n$.
Any help would be greatly appreciated.
Thank you in advance!
Update
In the meantime, I worked out the details of the proof myself. I'll post the full argument as an answer here soon.