Lemma predicateOnBasePointComponent (X:PointedType) (X' := BasePointComponent X) (pt' := basepoint X') (P:X'->hProp) (p:P pt') : ∏ x, P x. Proof. intros x. apply (squash_to_hProp (BasePointComponent_isBaseConnected _ x)); intros e. now induction e. Defined.