search

HoTT / book

A textbook on informal homotopy type theory
2.03k stars 359 forks source link

Assumption that `A // R` is a set #1126

Open FernandoChu opened 2 years ago

FernandoChu commented 2 years ago

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 commented 2 years ago

Sets and propositions were already discussed in chapter 3.

FernandoChu commented 2 years ago

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 commented 2 years ago

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 commented 2 years ago

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.