Lemma weq_subtypes_iff {X : UU} {S T : X -> UU} (HS : isPredicate S) (HT : isPredicate T) (HST : ∏ x, S x <-> T x) : (∑ x, S x) ≃ (∑ x, T x). Proof. apply (weq_subtypes' (idweq X)); assumption. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics.