Definition lift_pointed_PartialOrder_extract {X : hSet} (PX : pointed_PartialOrder X) (x : setcoprod X unitset) : X. Proof. induction x as [ x | ]. - exact x. - exact (⊥_{PX}). Defined.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets.Basics. Require Import UniMath.OrderTheory.Posets.MonotoneFunctions. Require Import UniMath.OrderTheory.Posets.PointedPosets.