search

HoTT / book

A textbook on informal homotopy type theory
2.03k stars 359 forks source link

Equivalence of path induction and based path induction #1117

Closed IanRay11 closed 1 year ago

IanRay11 commented 2 years ago

In Section 1.12.2 a proof of the equivalence of path induction and based path induction is provided. I am confused about two things in the latter direction (i.e. path induction implies based path induction.) This direction starts by defining a type and using an instance of path induction to obtain a function on an arbitrary path (and associated points) to the specfied type. In the forthcoming lines the 'definition is unfolded to expand the type' of the function. The next line is where my first question arises. The text says,

"Now given x:A and a p: a =_A x, we can derive the conlcusion of based path induction:".

It seems wrong to instantiate x here. Should we not instead be given the base point a? That is, should it not say,

"Now given a:A and a p: a =_A x, we can derive the conlcusion of based path induction:"?

Please let me know if I am missing something.

The second question is almost certainly an issue of my understanding. In both directions the book suggests alternative proofs which simpliy writes one induction principle in terms of the other. In the latter direction ind' (based path induction) is written in terms of ind (path induction) but strangely ind has 7 arguements. This does not match how ind is defined (only taking 5 arguments). Again, I am less sure that there is a mistake in the text here. I only attach it to my first inquiry in the hopes that someone can offer some insight.

mikeshulman commented 2 years ago

Well, we actually have to be given both a and x (and p). I think the phrasing was chosen to match the statement of based path induction in 1.12.1, where a is fixed from the outset, and we construct a function f depending on x and p. But I guess it might be clearer to write this out a bit more explicitly, e.g.

Now let a:A be fixed, and suppose we have C: Π(x:A) (a=x) -> U and c : C(a,refl) as in the statement of based path induction. We define the desired g : Π(x:A) Π(p:a=x) C(x,y) by g(x,p) = f(a,x,p,C,c).

Since the statement of based path induction uses f instead of g, it might also be better to use that here, and change the letter f used for the 5-argument function to something else.

However, this might be too radical a change. We could also just say "given a:A along with x:A and p:a=x". Any other opinions?

mikeshulman commented 2 years ago

For the second question, it's true that ind ordinarily has 5 arguments. But here we are applying ind in such a way that the result of applying it to those 5 arguments belongs to a function type that takes 2 more arguments. Since functions are all implicitly curried, that means this particular instance of ind does in fact take 7 arguments.

Would it be clearer to write the last two arguments separately? So the application of ind would end with ...,a,x,p)(C,c).

IanRay11 commented 2 years ago

Regarding your first comment: I agree that changing the name of f and g to match the initial statement of based path induction is a bit too radical. I think your final suggestion would have avoided my confusion.

We could also just say "given a:A along with x:A and p:a=x". Any other opinions?

Regarding your second comment: I feel that choosing to write the remaining two arguements in separate parenthesis is more suggestive to the reader that the result of induction is itself a function of two arguments. Although in retrospect if one type checks carefully enough they should be able to work this out on their own. I'm afraid I'm still lacking that necessary experience!

mikeshulman commented 2 years ago

Thanks for the feedback. I've made a PR with these suggestions.

IanRay11 commented 2 years ago

Going over this proof again with your insight is leading me to further questions. image In the left hand side of the equation we are given a family C and an element of the family c. On the right hand side the same C and c are the two arguments remaining after induction. It is my understanding that all other instances of C on the right hand side are bonded variables with in the scope of the functions being defined. Is that correct?

IanRay11 commented 2 years ago

Further, I believe this is contains a typo image I think it should say "... observe any such f can obtained as an instance of ind..." rather than ind' (where I am ommiting the subscripts).

Note this is from the first direction of the proof not the direction that we have been discussing at length above.

mikeshulman commented 2 years ago

Yes, that's right the other C's are bound. And I think you're right that that's a typo, I'll add it to the PR.