Homotopy Type Theory axiom R-flat > history (changes)

Showing changes from revision #3 to #4: Added | ~~Removed~~ | ~~Chan~~ged

~~Definition~~

~~Axiom~~

~~$\mathbb{R}\flat$~~ ~~: For a space~~ ~~$A$~~ , ~~$A$~~ ~~is discrete if and only if for every universe~~ ~~$\mathcal{U}$~~ ~~and every locally~~ ~~$\mathcal{U}$~~ ~~-small Dedekind real numbers~~ ~~$\mathbb{R}_\mathcal{U}$~~ ~~, the function~~ ~~$const: A \to (\mathbb{R}_\mathcal{U} \to A)$~~ ~~is an~~ ~~equivalence~~.

~~See also~~

contractibility of Dedekind real numbers

Dedekind real numbers

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)

Last revised on June 14, 2022 at 17:38:50. See the history of this page for a list of all contributions to it.