proposition: Lemma baseConnectedness X : isBaseConnected X -> isConnected X.
proof: Proof. intros p. split. - exact (hinhpr (basepoint X)). - intros x y. assert (a := p x); assert (b := p y); clear p. apply (squash_to_prop a); [apply propproperty|]; clear a; intros a. apply (squash_to_prop b); [apply propproperty|]; clear b; intros b. apply hinhpr. exact (!a@b). Defined.
imports: UniMath.MoreFoundations.Notations UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions