Skip to content
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.

Sign up for GitHub

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

Jump to bottom

Assumption that A // R is a set #1126

Open
FernandoChu opened this issue Sep 21, 2022 · 4 comments
Open

Assumption that A // R is a set #1126

FernandoChu opened this issue Sep 21, 2022 · 4 comments

Comments

@FernandoChu
Copy link
Contributor

FernandoChu commented Sep 21, 2022 •
edited
Loading

image
The proof of the theorem 6.10.6. uses implicitly that A // R is a set, since in general we need a embedding, not an injection. That A // R is a set can be proven from the fact that Prop is a set, together with some properties of sets (or, more generally, n-types), but these are introduced in the next chapter.

I think it's not easy to show that A // R is a set without knowing n-types, and this fact should be mentioned/suggested/assumed somewhere.
@mikeshulman
Copy link
Contributor

Sets and propositions were already discussed in chapter 3.

@FernandoChu
Copy link
Contributor Author

FernandoChu commented Sep 23, 2022 •
edited
Loading

Actually, you're right. I meant that the required properties were not introduced, but they were if you count the exercises, with the exception that Prop is a set, but that's immediate.

@FernandoChu
Copy link
Contributor Author

I mistook Prop being a set with isProp being a set. The latter is easy, but the former does not seem so (to me), and that's what we need here. Though, this is proven in Theorem 7.1.11 (later than when we need it), so I'm reopening.

@FernandoChu FernandoChu reopened this Sep 25, 2022
@mikeshulman
Copy link
Contributor

I'm surprised that this was left out of chapter 3, but it does seem to be missing. I suggest we just add it as an exercise, it's pretty easy.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@mikeshulman @FernandoChu