Proposition is_directed_comp {X Y : hSet} {PX : PartialOrder X} {PY : PartialOrder Y} (f : X → Y) (Hf : is_monotone PX PY f) {I : UU} {D : I → X} (HD : is_directed PX D) : is_directed PY (λ i, f(D i)). Proof. induction HD as [ H₁ H₂ ]. split. - exact H₁. - clear H₁. intros i j. specialize (H₂ i j). revert H₂. use factor_through_squash. { apply propproperty. } intros kp. apply hinhpr. refine (pr1 kp ,, _ ,, _). + apply Hf. exact (pr12 kp). + apply Hf. exact (pr22 kp). Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets.Basics. Require Import UniMath.OrderTheory.Posets.MonotoneFunctions.