proposition: Lemma predicateOnBasePointComponent (X:PointedType) (X' := BasePointComponent X) (pt' := basepoint X') (P:X'->hProp) (p:P pt') : ∏ x, P x.
proof: Proof. intros x. apply (squash_to_hProp (BasePointComponent_isBaseConnected _ x)); intros e. now induction e. Defined.
imports: UniMath.MoreFoundations.Notations UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions