Lemma baseConnectedness X : isBaseConnected X -> isConnected X. 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.