proposition: Proposition is_strict_and_monotone_lift_pointed_PartialOrder_dupl {X : hSet} (PX : pointed_PartialOrder X) : is_strict_and_monotone (lift_pointed_PartialOrder PX) (lift_pointed_PartialOrder (lift_pointed_PartialOrder PX)) (lift_pointed_PartialOrder_dupl PX).
proof: Proof. split. - intros [ x | [] ] [ y | [] ] p ; cbn in *. + exact p. + exact (fromempty p). + exact tt. + exact tt. - cbn. apply idpath. Qed.
imports: UniMath.MoreFoundations.All UniMath.OrderTheory.Posets.Basics UniMath.OrderTheory.Posets.MonotoneFunctions UniMath.OrderTheory.Posets.PointedPosets