I think the h‘s are correct. Any morphism in which either component is the identity must be homotopic to the identity, since homotopic is symmetric. In this proof, checking the h’s is easier.
Nice! I’m glad I asked, since I hadn’t realised those sufficient conditions for being homotopic to the identity. That’s useful in several proofs I suspect. (For anyone following along, I believe this only holds for a morphism from a frame to itself.)
minor typo:
should have p:E→W
Also I think later in that proof some of the h‘s (like in h0∘h1) should be g’s instead.
Fixed, Thanks.
I think the h‘s are correct. Any morphism in which either component is the identity must be homotopic to the identity, since homotopic is symmetric. In this proof, checking the h’s is easier.
Nice! I’m glad I asked, since I hadn’t realised those sufficient conditions for being homotopic to the identity. That’s useful in several proofs I suspect. (For anyone following along, I believe this only holds for a morphism from a frame to itself.)