proposition: 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: Proof. apply (weqbandf w). intros. apply weqiff. - apply HST. - apply HS. - apply HT. Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.Tactics