Corollary 2.4.4. (use of naturality and whiskering)

[IanRay11]

First I will provide a snippet of the text for easy reference.

The first thing I wish to address is the use of 'naturality' in the first line of the proof. I am vaugly familair with the use of this term from category theory, but I do not recall the term being discussed in HoTT and find it somewhat mystical here. Essentially, what (I think) is going on in the first part of the proof is that we are applying Lemma 2.4.3 with $g :\equiv \text{id}_A$ and $p :\equiv H(x)$ for some $x:A$. This automatically yields the diagram and equation stated in the first part of the proof. So what is the need for the opaque use of category theory terminology?

Edit: After burshing up on some category theory I do understand why this language is correct. But my contention still stands. If you are familiar with category theory the proof is already somewhat obvious and the use of the language reflects that. If you are not familiar with category theory then the language is not very helpful.

My second inquiry is likely something I am misunderstanding. The proof states, "We can now whisker by $(Hx)^{−1}$ to cancel $Hx$." Whiskering is mentioned first in Theorem 2.1.6. where we define "operations" between a path and 2-path with the intention of defining a "horizontal composition" of 2-paths. I'm unsure why we need to whisker by $(Hx)^{-1}$. Does $(Hx)^{-1}$ not exist by Lemma 2.1.1? Then we can simply apply the fact that if $p = q$ where $p,q: x = y$ and $r: y=z$ then $p \cdot r = q \cdot r$ together with the equation from the first part of the proof and all the neccesary paths from Lemma 2.1.4. to arrive at the desired identity.

[mikeshulman]

It's true in general that the book could stand more exposition of the category-theoretic terminology that it uses, but that's a big enough change that I doubt it will happen. I do think (unsurprisingly, since I'm a category theorist) that there's value in including the terminology -- in your case, it motivated you to (re)learn it! But perhaps we could add a parenthetical here noting that "naturality of H" is nothing other than the just-proved Lemma 2.4.3.

[mikeshulman]

I'm unsure why we need to whisker by (Hx)−1. Does (Hx)−1 not exist by Lemma 2.1.1? Then we can simply apply the fact that if p=q where p,q:x=y and r:y=z then p⋅r=q⋅r together with the equation from the first part of the proof and all the neccesary paths from Lemma 2.1.4. to arrive at the desired identity.

This is precisely a construction of whiskering. Theorem 2.1.6 defines it by direct path-induction on r, but you can also construct it out of other operations in the way you describe. (see below)

[IanRay11]

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 to a note or parenthesis (as you mentioned). A few paragraphs prior it is mentioned that a homotopy may be regarded as a natural isomorphism but no further context is given. For this reason I really do feel it is not sufficiently clear language for a proof.

[IanRay11]

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

[mikeshulman]

The operation of "whiskering by r" can be defined for all r at once by doing path induction on r, or it can be defined for any particular r by the operations you described.

[mikeshulman]

Sorry, my brain must have been turned off. The correct answer is that this:

the fact that if p=q where p,q:x=y and r:y=z then p⋅r=q⋅r

is whiskering.

[IanRay11]

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

[IanRay11]

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 $(X,\cdot)$ we would hope that if $x = y$ then $x \cdot z = y \cdot z$. (Well-defined maybe?)

Is this an example of some of the "coherence laws" that were mentioned following Lemma 2.1.4. and even the Lemma and Corollary in question?

[mikeshulman]

It's true, it's also definable as $\mathsf{ap}_{\lambda u. u\cdot z}(p)$ for $p:x=y$.