Lemma pointwisefamily_isdirected {D D' : dcpo} {I : UU} (F : I -> posetofdcpomorphisms D D') : isdirected F -> ∏ (d : D), isdirected (pointwisefamily F d). Proof. intros isdirec d. split. - exact (isdirected_inhabited isdirec). - intros i j. use factor_through_squash. + exact (directeduntruncated F i j). + apply isapropishinh. + intro direc. apply hinhpr. induction direc as [k ineqs]. exists k. unfold pointwisefamily. induction ineqs as [ineq1 ineq2]. split. * use ineq1. * use ineq2. + apply (isdirected_compatible isdirec). Qed.
Require Import UniMath.Foundations.All.