Definition make_pointed_PartialOrder {X : hSet} (RX : PartialOrder X) (x : X) (p : ∏ (y : X), RX x y) : pointed_PartialOrder X := RX ,, x ,, p.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets.Basics. Require Import UniMath.OrderTheory.Posets.MonotoneFunctions.