Lemma BasePointComponent_isBaseConnected (X:PointedType) : isBaseConnected (BasePointComponent X). Proof. intros [x' c']. change (basepoint (BasePointComponent X)) with (tpair (λ (y:X), ∥ basepoint X = y ∥) (basepoint X) (hinhpr (idpath (basepoint X)))). use (hinhfun _ c'); intro q. induction q. apply maponpaths. apply propproperty. Defined.