proposition: Lemma isConnected_isBaseConnected (X:PointedType) : isConnected X <-> isBaseConnected X.
proof: Proof. split. - intros [_ ic] x. use ic. - intros ibc. split. + exact (hinhpr (basepoint X)). + intros x y. apply (squash_to_hProp (ibc x)); intros p; apply (squash_to_hProp (ibc y)); intros q. exact (hinhpr (!p @ q)). Defined.
imports: UniMath.MoreFoundations.Notations UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions