Theorem 2.26.4

Question

Theorem 2.26.4

Closed this issue a year ago · 4 comments

Theorem 2.26.4 is formulated as an exercise, but the last sentence just before it reads "so we give a full proof", suggesting otherwise. I think a theorem is better here, as it would be a hard exercise, even though it is prepared by Exc. 2.17.12 (which is doable). BTW to avoid the formulation "each such factorization is equivalent" Thm. 2.26.4, I would propose defining the type of factorizations and prove that it is contractible. Perhaps also rephrase Exc. 2.17.12 in this sense.

UlrikBuchholtz commented a year ago

Done!

Answer 1 · 2023-01-12T15:28:27.000Z

I agree that we should define (in symbols) the type of factorizations the first time this is needed, in 2.17.12. Then we can be less precise later on.

Answer 2 · 2023-01-15T19:19:12.000Z

Done, see 25d93b7
However, working on this I changed my view on Thm. 2.26.4: it is premature, 0-connected and 0-trucated are not defined, and everything is done better in 3.9, Higher images. Hence my proposal is to delete Thm. 2.26.4.

Answer 3 · 2023-01-16T13:58:14.000Z

I swapped 2.26 and 2.27, since the old 2.26 mentioned general $n$-truncation (in old foornote 74), and this was defined in old 2.27. Also, old 2.26, at least in my view, works better as a last section of the chapter, a little informal with "stuff", "forgets at most" etc. Like the last lecture before a long holiday. So, after 2f8c893 we should still discuss what we want with Theorem (now) 2.27.4.