Lemma preservesdirectedlub_isdcpomorphism {D D' : dcpo} (f : D -> D') : isdcpomorphism' f -> isdcpomorphism f. Proof. intro preservesdireclub. split. - intros x y ineq. set (two := coprod unit unit). set (fam := (λ t : two, match t with | inl _ => x | inr _ => y end)). assert (isdirec : isdirected fam). { split. - apply hinhpr. exact (inl tt). - intros i j. apply hinhpr. exists (inr tt). induction i, j. + simpl. exact (ineq,,ineq). + simpl. split. ++ exact ineq. ++ apply isrefl_posetRelation. + simpl. split. ++ apply isrefl_posetRelation. ++ exact ineq. + simpl. split. ++ apply isrefl_posetRelation. ++ apply isrefl_posetRelation. } assert (islubfam : islub fam y). { split. - intro t. induction t. + simpl. exact ineq. + simpl. apply isrefl_posetRelation. - intros d ineqs. exact (ineqs (inr tt)). } set (islubfam' := preservesdireclub two fam isdirec y islubfam). apply (islub_isupperbound (f ∘ fam) islubfam' (inl tt)). - exact preservesdireclub. Qed.
Require Import UniMath.Foundations.All.