proposition: Lemma weqtotal2 {X Y:Type} {P:X->Type} {Q:Y->Type} (f : X ≃ Y) : (∏ x, P x ≃ Q (f x)) -> (∑ x:X, P x) ≃ (∑ y:Y, Q y).
proof: Proof. intros e. exists (λ xp, (f(pr1 xp),,e (pr1 xp) (pr2 xp))). exact (twooutof3c _ _ (isweqfibtototal P (Q ∘ f) e) (pr2 (weqfp f Q))). Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.Tactics