Homotopy Type Theory analytic Markov's principle > history (Rev #2, changes)

Showing changes from revision #1 to #2: Added | ~~Removed~~ | ~~Chan~~ged

~~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~~

axiom R-flat

intermediate value theorem

~~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 June 14, 2022 at 17:36:52 by Anonymous?. See the history of this page for a list of all contributions to it.