Lemma isaprop_isdirectedcomplete (X : Poset) : isaprop (isdirectedcomplete X). Proof. apply impred_isaprop; intro I. apply impred_isaprop; intro f. apply isapropimpl. apply invproofirrelevance. intros [u p] [v q]. apply total2_paths_equiv. exists (lubsareunique _ p q). apply proofirrelevance. apply isaprop_islub. Qed.
Require Import UniMath.Foundations.All.