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

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


< axiom R-flat


ℝ♭\mathbb{R}\flat: For a space AA, AA 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β†’(ℝ 𝒰→A)const: A \to (\mathbb{R}_\mathcal{U} \to A) is an equivalence.

See also


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