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

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.

• This is only my opinion, but (1) I can't think of any reason, and (2) I don't see how it does. Moreover, the abstract is already wrong: the book doesn't "justify" path induction by a homotopy interpretation, nor would that be incompatible with autonomy if it did. – Mike Shulman Jun 11 '15 at 19:18
• Perhaps you would prefer Patrick Walsh's paper 'Categorical Harmony and Path Induction' (academia.edu/22231067/Categorical_Harmony_and_Path_Induction). This was written as a Masters student under Steve Awodey's guidance. – David Corfield Sep 14 '16 at 4:34