0. Prove the groupoid laws for paths (slide 16) using path induction.

1. How does $\transport^B$ interact with the groupoid
   structure of paths? What about $\ap_f$? Prove your claims.

2. State and prove lemmas for decomposing a transport in function
   types and sigma types (the latter is messier).

3. Use paths over paths to state and prove that the empty vector is a
   unit for vector concatenation, and that vector concatenation is
   associative. (Hint: you will need to generalise ap_f to paths over
   paths.)