Definition weq_subtypes {X Y : UU} (w : X ≃ Y) (S : hsubtype X) (T : hsubtype Y) : (∏ x, S x <-> T (w x)) -> carrier S ≃ carrier T. Proof. intros eq. apply (weqbandf w). intro x. apply weqiff. - apply eq. - apply propproperty. - apply propproperty. Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.