Lemma doublelubdirected {D : dcpowithbottom} {I : UU} (F : I -> D -->D) (isdirec : isdirected F) (n : nat) (u u' : D) : islub (λ i : I, iter n (F i)) u' -> islub (λ j : I, (pr1) (F j) u') u -> islub (λ i : I, iter (S n) (F i)) u. Proof. intros islubu' islubu. split. - intro i. simpl. eapply istrans_posetRelation. + apply dcpomorphism_preservesorder. apply (islub_isupperbound _ islubu'). + apply (islub_isupperbound _ islubu). - intros d ineqs. apply (islub_isleast _ islubu). intro i. set (fam := λ i : I, iter n (F i)). assert (isdirec' : isdirected (λ i : I, iter n (F i))). { split. - exact (isdirected_inhabited isdirec). - intros i1 i2. use factor_through_squash. + exact (directeduntruncated F i1 i2). + apply isapropishinh. + intro direc. apply hinhpr. induction direc as [k ineqs']. exists k. split. * apply iter_preservesorder. exact (pr1 ineqs'). * apply iter_preservesorder. exact (pr2 ineqs'). + apply (isdirected_compatible isdirec). } eapply dcpomorphism_preserveslub. + exact isdirec'. + exact islubu'. + intro j. simpl. use factor_through_squash. * exact (directeduntruncated F i j). * apply propproperty. * intro direc. induction direc as [k ineqs']. eapply istrans_posetRelation. -- apply dcpomorphism_preservesorder. apply iter_preservesorder. apply (pr2 ineqs'). -- eapply istrans_posetRelation. ++ use (pr1 ineqs'). ++ exact (ineqs k). * apply (isdirected_compatible isdirec). Qed.
Require Import UniMath.Foundations.All.