3
$\begingroup$

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.

$\endgroup$
  • 3
    $\begingroup$ 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. $\endgroup$ – Mike Shulman Jun 11 '15 at 19:18
  • $\begingroup$ 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. $\endgroup$ – David Corfield Sep 14 '16 at 4:34
-1
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.