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

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


Axiom R ℝ♭ R\flat \mathbb{R}\flat: For a space AA, AA is discrete if and only if for every universe const 𝒰:Aβ†’(ℝ→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β†’(ℝ 𝒰→A)const: A \to (\mathbb{R}_\mathcal{U} \to A) is an equivalence , . whereℝ\mathbb{R} is the Dedekind real numbers.

See also


Revision on June 12, 2022 at 00:00:27 by Anonymous?. See the history of this page for a list of all contributions to it.