Showing changes from revision #1 to #2:
Added | Removed | Changed
Let be a continuous mapping on the space of Dedekind real numbers, and let be a term of the underlying homotopy type of the Dedekind real numbers. If we assume excluded middle, axiom R-flat, and the analytic Markov's principle, then if there exist points such that , then there exists a point such that
Let be a continuous mapping on the Dedekind real numbers, and let be a term of the underlying homotopy type of the Dedekind real numbers. number. If we assumeaxiom R-flat, then if there exist points such that , then for all terms there exists a point such that
Mike Shulman, Brouwer’s fixed-point theorem in real-cohesive homotopy type theory, Mathematical Structures in Computer Science Vol 28 (6) (2018): 856-941 (arXiv:1509.07584, doi:10.1017/S0960129517000147)
Matthew Frank, Interpolating Between Choices for the Approximate Intermediate Value Theorem, Logical Methods in Computer Science Vol 16 (3) (July 14, 2020) (arXiv:1701.02227, doi=10.23638/LMCS-16(3:5)20202020))