fact: Definition basePointComponent_inclusion {X:PointedType} (x : BasePointComponent X) : X := pr1 x.
imports: UniMath.MoreFoundations.Notations UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions