Comments (7)
The Escardo-Simpson or higher inductive-inductive Cauchy reals could be done in predicative constructive set theory by adding an axiom and possibly any relevant signatures to the set theory which says that there is an initial Cauchy structure as defined by Booij, translating the relevant notions to first-order logic (i.e. contractible -> there exists a unique element, etc).
I don't see this as any different from the predicative constructivists who add an initial sigma-frame (which is a HIIT in HoTT) to their predicative constructive set theory to work with Dedekind-style reals.
from book.
As a side note, my former PhD student @abooij tried to publish this, but it was not deemed to be deep enough and worthy of publication by the referees. Perhaps you should try again, @abooij .
Another one from James Hanson:
In set-theoretic foundations, the definition of the real numbers as equivalence classes of
Cauchy sequences requires either the law of excluded middle or the axiom of (countable)
choice to be well-behaved. But with higher inductive types, we can give a version of this
definition which is well-behaved and avoids any choice principles.Now that we know that The HoTT reals coincide with the Escardó-Simpson reals, it follows that an equivalent construction to the HIIT reals could be done in impredicative constructive set theory by taking the Cauchy closure of the rationals inside the Dedekind reals. So while the statement is, strictly speaking, true, it may give a misleading impression of what is possible in set theory vs. in HoTT. I'm not sure how best to remedy this, especially since it depends on impredicativity, while predicativity hasn't been mentioned yet. Perhaps a footnote?
from book.
As I see things, most HoTT/UF practicioners, and also the HoTT book, try to be predicative. Of course, an exception is the UniMath project. Moreover, the correspondence of HoTT/UF with ∞-toposes relies fundamentally on impredicativity. So perhaps the HoTT book should explicitly say something about this? I have to say that, for myself, it took me a while to figure out what exactly was going on regarding (im)predicativity in HoTT/UF.
from book.
(Im)predicativity, in the sense relevant here (i.e. propositional resizing), is mentioned in section 3.5. I just meant it hadn't been mentioned yet in the introduction, which is where this comment occurs.
from book.
In set-theoretic foundations, the definition of the real numbers as equivalence classes of Cauchy sequences requires either the law of excluded middle or the axiom of (countable) choice to be well-behaved.
Also, this isn't true, either in set theory or in type theory. On one hand, one can use weaker choice principles like analytic LPO or just outright stipulate that the Dedekind and Cauchy reals coincide. On the other hand, even with countable choice there are issues with topology and pointwise analysis where one needs to also add the fan theorem.
But with higher inductive types, we can give a version of this definition which is well-behaved and avoids any choice principles.
What does well-behaved mean in this context? You can't use the higher inductive-inductive Cauchy reals in the real cohesion axiom since it doesn't have the same topology as the Dedekind reals, you have to use the Dedekind reals instead. In this sense, the Cauchy reals constructed in chapter 11 as a higher inductive-inductive type aren't well-behaved, and one has to use Cauchy nets or Cauchy filters if one wants a well-behaved type of reals.
Then there are the locale theorists who would argue that one should be using the locale of real numbers instead of the Cauchy, Escardo-Simpson, or Dedekind reals since the space of points isn't well behaved constructively compared to locales.
from book.
In set-theoretic foundations, the definition of the real numbers as equivalence classes of Cauchy sequences requires either the law of excluded middle or the axiom of (countable) choice to be well-behaved.
Also, this isn't true, either in set theory or in type theory. On one hand, one can use weaker choice principles like analytic LPO or just outright stipulate that the Dedekind and Cauchy reals coincide. On the other hand, even with countable choice there are issues with topology and pointwise analysis where one needs to also add the fan theorem.
The usual LPO for natural numbers should suffice here, even predicatively. The HoTT book only assumes that
from book.
Countable choice does suffice.
from book.
Related Issues (20)
- Assumption that `A // R` is a set HOT 4
- Rules for universes in Appendix A.2 are incomplete HOT 3
- identity type usage HOT 19
- Augment assumptions for Thm 5.4.4, 5.4.5, and 5.4.7 HOT 19
- Typos in proof of Lemma 10.3.12 HOT 5
- Use parentheses in the proof of Lemma 2.1.4(iii) HOT 3
- Cumulativity of the universe hierarchy HOT 4
- CI problem: "dubious ownership" HOT 1
- Provided Hashes in errata.pdf Not Found HOT 2
- Errata PDF unreadable
- Corollary 8.8.5 HOT 4
- Lemma 8.5.9 is missing a label
- Nightly builds pdfs are dead links HOT 8
- Exercise 7.3 could be made stronger
- Indexing of maps in fiber and exact sequences HOT 3
- proof-theoretic consistency in the introduction HOT 6
- cardinal numbers in the introduction HOT 5
- Switch to using truncated logic as default in the book HOT 2
- max and sup HOT 9
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from book.