A proof of constructive version of Brouwer's fixed point theorem with uniform sequential continuity (Q420168)

Summary: It is often said that Brouwer's fixed point theorem cannot be constructively proved. On the other hand, Sperner's lemma, which is used to prove Brouwer's theorem, can be constructively proved. Some authors have presented a constructive (or an approximate) version of Brouwer's fixed point theorem using Sperner's lemma. They, however, assume uniform continuity of functions. We consider uniform sequential continuity of functions. In classical mathematics, uniform continuity and uniform sequential continuity are equivalent. In constructive mathematics à la Bishop, however, uniform sequential continuity is weaker than uniform continuity. We will prove a constructive version of Brouwer's fixed point theorem in an \(n\)-dimensional simplex for uniformly sequentially continuous functions. We follow the Bishop style constructive mathematics.