Homotopy Type Theory contractibility of Dedekind real numbers > history (Rev #3, changes)

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

~~Definition~~

~~Axiom: The~~

~~shape~~ of ~~$\mathbb{R}$~~ is ~~contractible~~:

~~$p:isContr(\esh(\mathbb{R}))$~~
~~This statement can be derived from axiom R-flat~~
~~See also~~

axiom R-flat

Dedekind real numbers

continuous mapping

~~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:33:35 by Anonymous?. See the history of this page for a list of all contributions to it.