Judgmental vs. Propositional Uniqueness in HoTT book.

[MaximJeffs]

On page 30, the HoTT book claims that we can construct the term uniq_1 using the defining equation uniq_1(*) :=refl*. But this already seems to assume a stronger form of uniqueness for 1, since refl* is only well-typed if x is judgmentally equal to * for all x:1, but yet in constructing uniq_1 we are only asserting the weaker statement that every x:1 is propositionally equal to *.
If the homotopy-theoretic interpretation is that 1 is the one-point space, surely we want all points to be (judgmentally) equal, rather than just joined by a path?