Definition totalAssociativity {X:UU} {Y: ∏ (x:X), UU} (Z: ∏ (x:X) (y:Y x), UU) : (∑ (x:X) (y:Y x), Z x y) ≃ (∑ (p:∑ (x:X), Y x), Z (pr1 p) (pr2 p)). Proof. intros. simple refine (_,,isweq_iso _ _ _ _). { intros [x [y z]]. exact ((x,,y),,z). } { intros [[x y] z]. exact (x,,(y,,z)). } { intros [x [y z]]. reflexivity. } { intros [[x y] z]. reflexivity. } Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics.