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