Definition islowerbound_subtype_equiv {A B : hsubtype P} : (A ≡ B) -> islowerbound_subtype A ≡ islowerbound_subtype B. Proof. intros e_A_B x; split; intros x_lb [y H_y]; refine (x_lb (_,,_)); 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.