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