Corollary 8.8.5

[blindFS]

"the hypotheses imply that $\pi_k(fib_f {f(a)})=0$ for all $k\le n$ and $a:A$, and that $||{fib_f{f(a)}}||_0$ is contractible.
Since $\pi_k(fib_f {f(a)}) = \pi_k(||{fib_f{f(a)}}||_n)$ for $k\le n$, and $||{fib_f{f(a)}}||_n$ is $n$-connected, by 8.8.4 it is contractible for any $a$."

I have following questions about this proof:

1. If $||{fib_f{f(a)}}||_n$ is $n$-connected, then it is contractible by definition of n-connectedness, why do we need 8.8.4? My understanding is that here the "n-connected" should be "a n-type", matching the presumption of corollary 8.8.4
2. How to prove the following statement $\pi_k(fib_f {f(a)}) = \pi_k(||{fib_f{f(a)}}||_n)$ for $k\le n$? The closest lemma I can find in this book is lemma 8.3.2, which again requires that $||{fib_f{f(a)}}||_n$ is $n$-connected, i.e. the missing part of the proof
3. Where is the assumption (iii) used in this proof?

[mikeshulman]

1. You're right, it should be "is an n-type".
2. This follows from the commutation of truncations with loop-spaces, Corollary 7.3.14: $\pi_k(\Vert A\Vert_n ) = \Vert \Omega^k (\Vert A\Vert_n) \Vert_0 = \Vert \Vert \Omega^k A \Vert_{n-k} \Vert_0 = \Vert \Omega^k A \Vert_0$. However, at the moment I don't see anywhere that this is stated explicitly. If it isn't, we should probably add it.
3. In the second sentence, where the LES is applied to get $\pi_{k}(fib_f(f(a))) = 0$ for $k\le n$. In the case $k=n$, we get this from the part of the LES that looks like $\pi_{n+1}(A) \to \pi_{n+1}(B) \to \pi_n(\mathsf{fib}_f(f(a))) \to \pi_n(A) \to \pi_n(B)$. Here (iii) gives surjectivity of the first map, so that the second map is zero; and injectivity of the fourth map (which is part of (ii)) makes the third map zero, hence the middle object is also zero.

[blindFS]

Thanks for the detailed explanations, closing.

[mikeshulman]

If you don't mind, I'm going to reopen it because (1), at least, is a typo that should be fixed.

[blindFS]

Sure