Lemma isaprop_preserveslub {P Q : Poset} (f : P -> Q) {I : UU} (u : I -> P) : isaprop (preserveslub f u). Proof. apply impred_isaprop; intro v. apply isapropimpl. apply isaprop_islub. Qed.
Require Import UniMath.Foundations.All.