[[!redirects Sandbox > history]] [[!redirects Sandbox]] < [[nlab:Sandbox]] Axiom of real cohesion, but where the real numbers are defined as the terminal Archimedean ordered field. Valid predicatively, and impredicatively one could prove that the real numbers are Dedekind complete. Most of real-cohesive homotopy type theory doesn't require that the Archimedean ordered field be Dedekind complete. Rather contractibility of shape and Cauchy completeness suffices for most proofs. The former comes from $\mathbb{R} \flat$ and the latter comes from $\mathbb{R}$ being an algebra for the endofunctor $K \mapsto \mathcal{C}(K)$ which takes Archimedean ordered fields to its Archimedean ordered field of equivalence classes of Cauchy sequences, which comes from $\mathbb{R}$ being a terminal Archimedean ordered field. The endofunctor $K \mapsto \mathcal{C}(K)$ exists in any $\Pi W$-pretopos. The fact that $\mathbb{R}$ is terminal in the category of Cauchy complete Archimedean ordered fields means that it is initial if and only if the limited principle of omniscience is true. Of course we also require our Archimedean ordered fields to from a pseudolattice with $\min$ and $\max$ functions. * [[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](https://arxiv.org/abs/1509.07584), [doi:10.1017/S0960129517000147](https://doi.org/10.1017/S0960129517000147)) Impredicativity is actually needed to define inductive covers and formal topologies. Because, without universes, the only way to index by subtypes and quantify over subtypes is to use functions into the type of all propositions. category: redirected to nlab