Ladyman's alternative justification for path induction in Homotopy Type Theory

Question

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.

Answer 1

1) I can't speak for Ladyman and Presnell here, but I think the notion of identity is a philosophically poignant case study for Hott. The identity type's justification and presentation is perhaps the oddest, from a classically philosophical point of view, if we use the homotopy interpretation. The centrality of identity in HoTT and philosophy might speak to the authors' choice to focus on it.

2) And they don't want UIP in its usual sense of Uniqueness of Identity Proofs. They want something like it that doesn't ruin intensionality but can also be philosophically justified, using their standards for that justification. They're trying to show that contractability and transport are justified in a philosophically safe way since the combination of these two is equivalent to path induction. Once they justify these two principles -- they use different names -- they justify path induction.

That's how I understand it, at least.