Introduction to Homotopy Type Theory, Chapter 2

[VojtechStep]

Still a draft with a long way to go. This is now my procrastination fuel.

Typos/potential oversights found during transcription:

• 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.