IanRay11

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...

Going over this proof again with your insight is leading me to further questions.  In the left hand side of the equation we are given a family C and...

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

I like the use of the categorical language as long as it parallels the necessary and self contained information that comes before. I agree use of naturality should be relegated...

So if I instead whiskered by $(Hx)^{-1}$ would I be doing path induction on... $(Hx)^{-1}$?

I think I was just starting to realize this! Thank you for clarifying!

Whiskering is admittedly a very cool name, but is it not a very desirable property of how identity and path composition should play together? For any set with binary operation...

Ahhhh, I see. I assume this notion is discussed further in either Chapter 3 Sets and Logic or Chapter 4 Equivalences? My real issue is the lack of assurance that...

Yes. I think that would be fine. I have just convinced myself that the two are logically equivalent (functions going both ways as defined earlier). But your point about only...

Okay. I've done everything Martin suggested so I will now ping @tomdjong (but please ignore until after break :))