proposition: 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: 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.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.OrderTheory.Posets.Basics