Definition sumofmaps_assoc_right {X Y Z T : UU} (f : X -> T) (g : Y -> T) (h : Z -> T) : sumofmaps f (sumofmaps g h) ∘ coprodasstor _ _ _ ~ sumofmaps (sumofmaps f g) h. Proof. intros. intros [[x|y]|z]; apply idpath. Defined.