-
Notifications
You must be signed in to change notification settings - Fork 354
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Set or h-set #5
Comments
I think we decided to just say 'set', because internally to type theory
|
So does that mean we should erradicate h-sets? And we have two definitions... |
Yes. The definitions in chapter 5 should probably be changed to recall
|
I renamed h-prop and h-set in chapter 5 (commit d4ecd0e) but didn't point the definitions to chapter 2 as Mike suggested. (I only saw this issue afterwards...) |
Chapter 5 now points to chapter 2 appropriately. |
In revising the set theory chapter I discovered Definition 2.7.1 of a "set" and Definition 5.3.9 of "h-set". What is the official terminology? Should I say "set" or "h-set"?
The text was updated successfully, but these errors were encountered: