proposition: Lemma isaprop_isdirected (f : I -> X) : isaprop (isdirected f).
proof: Proof. apply isapropdirprod. - apply isapropishinh. - apply impred_isaprop; intro i; apply impred_isaprop; intro j. apply isapropishinh. Qed.
imports: UniMath.Foundations.All