Proposition lift_isPartialOrder {X : hSet} (PX : PartialOrder X) : isPartialOrder (lift_hrel PX). 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.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets.Basics. Require Import UniMath.OrderTheory.Posets.MonotoneFunctions. Require Import UniMath.OrderTheory.Posets.PointedPosets.