search

HoTT / book

A textbook on informal homotopy type theory
2.04k stars 360 forks source link

Wording in exercise 8.8 "junior Hopf fibration" #438

Closed midfield closed 11 years ago

midfield commented 11 years ago

Exercise 8.8 ("the junior Hopf fibration") states

"define the junior Hopf fibration as a fibration (that is, a type family) over S^1 whose fibers are S^0"

Following the book's conventions, this probably should be reworded to something like

"whose fiber over the basepoint is S^0"

or

"whose fibers are merely equivalent to S^0"

andrejbauer commented 11 years ago

I don't think so. It should be possible to prove that forall x : S1, JuniorHopf(x) ≃ S0. What makes you think that the are "merely" equivalent to S0?

mikeshulman commented 11 years ago

It should be possible to prove that forall x : S1, JuniorHopf(x) ≃ S0.

If that were the case, then by function extensionality, JuniorHopf would be a constant type family, which it's not supposed to be.

andrejbauer commented 11 years ago

Hmm, I should learn some homotopy type theory. So what is the correct formulation of the exercise then?

mikeshulman commented 11 years ago

I would probably say "whose fiber over the basepoint is S^0".

mikeshulman commented 11 years ago

Actually, the senior Hopf fibration (Theorem 8.5.1) has the same problem!