Proposition eq_PartialOrder {X : hSet} {PX PX' : PartialOrder X} (p : is_monotone PX PX' (λ x, x)) (q : is_monotone PX' PX (λ x, x)) : PX = PX'. Proof. use subtypePath. { intro. apply isaprop_isPartialOrder. } use funextsec ; intro. use funextsec ; intro. use weqtopathshProp. use weqimplimpl. - apply p. - apply q. - apply (pr1 PX). - apply (pr1 PX'). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets.Basics.