proposition: Proposition lift_isPartialOrder {X : hSet} (PX : PartialOrder X) : isPartialOrder (lift_hrel PX).
proof: Proof. repeat split. - intros [ x₁ | [] ] [ x₂ | [] ] [ x₃ | [] ] p q ; cbn in *. + exact (trans_PartialOrder PX p q). + exact q. + exact (fromempty p). + exact p. + exact tt. + exact tt. + exact tt. + exact tt. - intros [ x | [] ] ; cbn. + exact (refl_PartialOrder PX x). + exact tt. - intros [ x | [] ] [ y | [] ] p q ; cbn in *. + apply maponpaths. exact (antisymm_PartialOrder PX p q). + exact (fromempty p). + exact (fromempty q). + apply idpath. Qed.
imports: UniMath.MoreFoundations.All UniMath.OrderTheory.Posets.Basics UniMath.OrderTheory.Posets.MonotoneFunctions UniMath.OrderTheory.Posets.PointedPosets