I'm confused by the main point of this paper: http://philsci-archive.pitt.edu/11079/1/Identity_in_HTT_public.pdf
The authors ask whether HoTT is a valid foundation for all of mathematics in a certain strong sense. They identify the justification of path induction as crucial point. Then, it is shown that path induction follows from the uniqueness principle for identity types (UIP) and substitution of equal expressions ("transport" in HoTT).
Two Questions:
1) Why does the question arise at all? Why is it path induction and not induction on any other type that needs further justification? And more important 2) How does the result help? I thought that the point of HoTT is that we dont want UIP because "higher dimensional equalities" are interesting and more diverse.
Confused. Thanks for tipps.