Homotopy Type Theory axiom R-flat > history (Rev #3, changes)

Showing changes from revision #2 to #3: Added | Removed | Changed

Definition

Axiom $\mathrm{<span><del\; class="diffmod">\; R</del><ins\; class="diffmod">\; ℝ</ins></span>}♭$ R\flat \mathbb{R}\flat: For a space $A$, $A$ is discrete if and only if for every universe$\mathrm{<span><del\; class="diffmod">\; const</del><ins\; class="diffmod">\; 𝒰</ins></span>}:A\to (ℝ\to A)$ const: \mathcal{U} A \to (\mathbb{R} \to A) is and an 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 , . where$\mathbb{R}$ is the Dedekind real numbers.

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)