Lemma dcpomorphism_preservesdirected {D D' : dcpo} (f : dcpomorphism D D') {I : UU} {u : I -> D} : isdirected u -> isdirected (pr1 f ∘ u). Proof. intro isdirec. split. - exact (isdirected_inhabited isdirec). - intros i j. apply (@factor_through_squash (directeduntruncated u i j)). + apply isapropishinh. + intro direc. apply hinhpr. induction direc as [k ineqs]. split with k. split. * apply dcpomorphism_preservesorder. exact (pr1 ineqs). * apply dcpomorphism_preservesorder. exact (pr2 ineqs). + exact (isdirected_compatible isdirec i j). Qed.
Require Import UniMath.Foundations.All.