This seems all well thought-out and the drawings are very well-made. However, descriptions like "We make a path p : true ≡ false from the assumed path (homotopy) h : Refl ≡ loop by constructing a non-trivial Bool-bundle over the circle, hence obtaining a map ( Refl ≡ loop ) → ⊥." are largely incomprehensible for people without an undergraduate in mathematics.<p>The combination "try to understand the math concepts that are not explained", "deal with a programming language and syntax I've never seen before" and "deal with emacs" quickly extinguished any interest I had as a mere physicist.<p>That being said, I think the core issue is that I'm not in the target audience. At the same time, it's being posted in a more general forum, and I think it's important for others to know that thye shouldn't feel too frustrated when they can't figure out the goal (let alone the solution) to the exercises.