Assumption that A // R is a set

[FernandoChu]

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]

Sets and propositions were already discussed in chapter 3.

[FernandoChu]

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]

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.

[mikeshulman]

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.