Homotopy Type Theory analytic Markov's principle > history (Rev #1)

Definition

The analytic Markov’s principle states that for all points $x$ in the space of real numbers, if $x \leq 0$ is false, then $x \gt 0$ .

\prod_{x:\mathbb{R}} ((x \leq 0) \to \emptyset) \to (x \gt 0)

See also

References

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)

Revision on April 22, 2022 at 23:40:00 by Anonymous?. See the history of this page for a list of all contributions to it.