Definition hconj_equiv {X:UU} {A A' B B' : hsubtype X} (e_A : A ≡ A') (e_B : B ≡ B') : (A ∩ B) ≡ (A' ∩ B'). Proof. intros x; split; intros [? ?]; split; try apply e_A; try apply e_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.