Definition weq_total2_prod {X Y} (Z:Y->Type) : (∑ y, X × Z y) ≃ (X × ∑ y, Z y). Proof. intros. simple refine (make_weq _ (isweq_iso _ _ _ _)). { intros [y [x z]]. exact (x,,y,,z). } { intros [x [y z]]. exact (y,,x,,z). } { intros [y [x z]]. reflexivity. } { intros [x [y z]]. reflexivity. } Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics.