proposition: Lemma BasePointComponent_isweq {X:PointedType} (bc : isBaseConnected X) : isweq (@basePointComponent_inclusion X).
proof: Proof. use isweqpr1. intros x. apply iscontraprop1. - apply propproperty. - exact (bc x). Defined.
imports: UniMath.MoreFoundations.Notations UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions