Proposition eq_pointed_PartialOrder_monotone {X : hSet} {PX PX' : pointed_PartialOrder X} (p : is_monotone PX PX' (λ x, x)) (q : is_monotone PX' PX (λ x, x)) : PX = PX'. Proof. use subtypePath. { intro. apply isaprop_bottom_element. } use eq_PartialOrder. - apply p. - apply q. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets.Basics. Require Import UniMath.OrderTheory.Posets.MonotoneFunctions.