fact: Definition isConnected X : hProp := ∥ X ∥ ∧ ∀ (x y:X), ∥ x = y ∥.
imports: UniMath.MoreFoundations.Notations UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions