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