search

HoTT / book

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

Incorrect diagram for Example 8.7.16 #1163

Open roconnor opened 2 months ago

roconnor commented 2 months ago

I don't know anything about CW complexes but I think the diagram should have the left hand arrow in the pushout being pr₁ : S₁ × 𝕊⁰ → S₁, and similarly for the second diagram.

mikeshulman commented 2 months ago

Hmm, yes, I think you're right. Would you like to submit a pull request?