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. split. - intros [ x | [] ] [ y | [] ] p ; cbn in *. + exact p. + exact (fromempty p). + exact tt. + exact tt. - cbn. 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.