Comments (5)
from book.
from book.
How about this:we canobtain such represen-tatives in a natural way by truncating the universe.
For what it's worth I don't really find this to be an acceptable alternative. The special named type-theoretic universes in most type theories aren't a semantically defined class; they're just particular types that have been selected syntactically to be called universes and are assumed to have the required closure properties. There's nothing in most type theories that prevents the existence of a type in U_1 that codes what by rights should be a proper sub-universe of U_0 but which isn't 'officially' a universe. So given this, why would it be any less natural for a set theory to add a special class of explicitly named inaccessible sets?
from book.
Also the word "representatives" is perhaps a bit misleading to use at all because with this approach we are not selecting canonical "representatives of equivalence classes" for isomorphism of sets but defining a notion of "cardinal number" that doesn't need such representatives.
The way I see it, the mathematical points are:
- In HoTT, the naturally-defined "type of well-ordered sets" is already a set (in the next universe) and contains exactly one element of each isomorphism class, so we can also call it "the type of ordinal numbers" without needing to specify canonical representatives of well-ordered sets like von Neumann ordinals. However, I think this doesn't really pertain at all to constructivity, which is the point of this section of the introduction, since von Neumann ordinals aren't really a place where constructivity makes things more difficult in set theory: the constructive theory of von Neumann ordinals is fairly well-developed and unproblematic, we just have to use the correct notion of well-foundedness.
- In HoTT, the 0-truncation of a universe acts as a type of cardinal numbers in that universe. In set theory one usually defines cardinal numbers to be initial ordinals (which requires AC) or using Scott's trick (which requires the axiom of foundation) -- and there are other methods that require less, though still something -- but one could also stipulate a tower of universes like in type theory and obtain a notion of cardinal number in some universe by quotienting the universe by equinumerosity. So the difference between HoTT and set theory here is (1) the use of specified universes, which is standard even in non-univalent type theory and could also be done in set theory, although it isn't usually, and (2) the fact that writing down the 0-truncation doesn't refer explicitly to equinumerosity since that was built into the identity types by univalence.
Do we agree on that, and the question is just what to say in the introduction that is concise and correct?
from book.
Incidentally, Peter Aczel has a paper in which he introduced a couple of specific constructive set theories with explicitly named universes:
Aczel, P. (1999). On Relating Type Theories and Set Theories. In: Altenkirch, T., Reus, B., Naraschewski, W. (eds) Types for Proofs and Programs. TYPES 1998. Lecture Notes in Computer Science, vol 1657. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48167-2_1
from book.
Related Issues (20)
- 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
- real numbers in the introduction HOT 7
- Switch to using truncated logic as default in the book HOT 2
- max and sup HOT 9
- Exercise 11.6 seems to need WLPO not LPO HOT 3
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.