Lemma ispartialorder_pointwiseorder (D D' : dcpo) : isPartialOrder (pointwiseorder D D'). Proof. split. - split. + intros f g h ineq1 ineq2 d. eapply istrans_posetRelation. ++ use ineq1. ++ use ineq2. + intros f p. apply isrefl_posetRelation. - intros f g ineq1 ineq2. apply total2_paths_equiv. assert (funeq : pr1 f = pr1 g). { use funextfun; intro d. apply isantisymm_posetRelation. - use ineq1. - use ineq2. } exists funeq. apply proofirrelevance, isaprop_isdcpomorphism. Qed.
Require Import UniMath.Foundations.All.