Definition isupperbound_subtype_equiv {A B : hsubtype P} : (A ≡ B) -> isupperbound_subtype A ≡ isupperbound_subtype B. Proof. intros e_A_B x; split; intros x_ub [y H_y]; refine (x_ub (_,,_)); apply e_A_B; assumption. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.OrderedSets.WellOrderedSets. Require Import UniMath.OrderTheory.DCPOs.AlternativeDefinitions.Dcpo. Require Import UniMath.OrderTheory.Posets.Subposets.