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