Definition pointed_PartialOrder (X : hSet) : UU := ∑ (RX : PartialOrder X), bottom_element RX.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets.Basics. Require Import UniMath.OrderTheory.Posets.MonotoneFunctions.