Definition lift_hrel {X : hSet} (PX : hrel X) : hrel (setcoprod X unitset). Proof. intros x₁ x₂. induction x₁ as [ x₁ | ]. - induction x₂ as [ x₂ | ]. + exact (PX x₁ x₂). + exact hfalse. - exact htrue. Defined.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets.Basics. Require Import UniMath.OrderTheory.Posets.MonotoneFunctions. Require Import UniMath.OrderTheory.Posets.PointedPosets.