Lemma weq_subtypes' {X Y : UU} (w : X ≃ Y) {S : X -> UU} {T : Y -> UU} (HS : isPredicate S) (HT : isPredicate T) (HST : ∏ x : X, S x <-> T (w x)) : (∑ x, S x) ≃ (∑ y, T y). Proof. apply (weqbandf w). intros. apply weqiff. - apply HST. - apply HS. - apply HT. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics.