proposition: Proposition eq_pointed_PartialOrder_strict_and_monotone {X : hSet} {PX PX' : pointed_PartialOrder X} (p : is_strict_and_monotone PX PX' (λ x, x)) (q : is_strict_and_monotone PX' PX (λ x, x)) : PX = PX'.
proof: Proof. use eq_pointed_PartialOrder_monotone. - apply p. - apply q. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.OrderTheory.Posets.Basics UniMath.OrderTheory.Posets.MonotoneFunctions