In Mike Shulman's article Brouwer’s fixed-point theorem in real-cohesive homotopy type theory, the fundamental axiom adopted for his real-cohesive homotopy type theory (axiom $\mathbb{R}\flat$), which states that the only (continuous) functions from the Dedekind real numbers to every discrete cohesive type $A$ are the constant functions to $A$, requires defining the Dedekind real numbers. However, in predicative mathematics, without assuming propositional resizing or an alternative like replacement or subset collection in the type theory (making all sets of Dedekind real numbers equivalent to each other), the Dedekind real numbers are
- no longer small relative to the propositions from which the Dedekind cuts are defined from, as the set of Dedekind cuts (which are pairs of subsets/predicates of a dense strict linear order) is not small, but only locally small, relative to the propositions
- no longer unique, as a result of point 1., there exists a set of Dedekind real numbers for every internal universe in the ambient universe, and we can no longer speak of the Dedekind real numbers. If there are no internal universes, we cannot even define a set of Dedekind real numbers
- assuming there is at least one internal universe in the ambient universe, no set of Dedekind real numbers is even guaranteed to be terminal in the ambient universe, depending upon the internal universe hierarchy in the ambient universe: Suppose one has an internal hierarchy of universes indexed by the natural numbers, where for natural numbers $n$ and $m$, $U_n$ embeds into $U_m$ for $n \leq m$. Then for every set of Dedekind real numbers $\mathbb{R}_n$ defined from propositions in $U_n$ there is a larger set of Dedekind real numbers $\mathbb{R}_m$ defined from propositions in $U_m$, where $\mathbb{R}_n$ embeds in $\mathbb{R}_m$, and thus there is no such terminal Archimedean ordered field in the ambient universe.
In such a case, how would one even go about even defining axiom $\mathbb{R}\flat$? Do we simply get multiple inequivalent versions of axiom $\mathbb{R}\flat$ of varying strengths? Suppose one simply selects a random set of Dedekind real numbers $\mathbb{R}$ for axiom $\mathbb{R}\flat$, how exactly does that particular axiom $\mathbb{R}\flat$ interacts with sets of Dedekind real numbers $\mathbb{R}'$ where $\mathbb{R}$ embeds into $\mathbb{R}'$ but it isn't possible to prove (without propositional resizing/subset collection/etc) that $\mathbb{R}$ is equivalent to $\mathbb{R}'$, as well as sets of Dedekind real numbers $\mathbb{R}^\dagger$ where $\mathbb{R}^\dagger$ embeds into $\mathbb{R}$?
Best Answer
My suggestion would be to start from your intended semantics. First ask what kind of "predicative topos" you have in mind where the theory you're asking about would have a model, and construct a particular such category that you're interested in. Then once you have a model, ask what axioms that model satisfies. That's the motivation for the original axiom $\mathbb{R}\flat$: it holds in an intended model of Euclidean-topological infinity-groupoids.