Introduction to Homotopy Type Theory, Sections 9 to 13

[VojtechStep]

Progress towards #1925.

Typos/potential oversights found during transcription (I haven't checked if they were already fixed in the physical book):

• Page 114, Exercise 9.7 (e), typo in condition (ii) — as stated is provably false (counterexample included), alpha and beta need to assume points in the codomains, not domains.
• Page 136, Example 11.6.4, "alternative characterization of the fiber" should probably say "alternative characterization of equality of the fiber"
• -----, proving the last equivalence seems to require equiv-right-transpose-eq-concat, which has not been stated.
• Page 138, Exercise 11.10, this and other exercises ask the reader to "show that the following are equivalent"; this can mean to show inverse implications, but it's also possible to interpret it as showing a literal equivalence. That's also possible, but would require some understanding of hProps and proofs of being one, which only comes up in the next section. What's the intention here? I'm not sure if the snippet should import equiv-is-path-split-is-equiv.
• Page 148, Theorem 12.4.7, last step of equivalence reasoning is on a new page.
• Page 149, Exercise 12.3 (a), "injective map" is used but not defined previously.
• Page 154, proof of Theorem 13.1.2 has a linebreak between a type in displaymath and "is contractible", which is quite confusing.
• Page 170, Exercise 13.14 (b), typo "retr(h) is a retract of sec(f)" instead of "is a retract of retr(f)".

[VojtechStep]

I'm opening this for review, hopefully the next batch won't rot for a year 💀