Lemma BasePointComponent_isweq {X:PointedType} (bc : isBaseConnected X) : isweq (@basePointComponent_inclusion X). Proof. use isweqpr1. intros x. apply iscontraprop1. - apply propproperty. - exact (bc x). Defined.