Definition homotcoprodfcomp {X X' Y Y' Z Z' : UU} (f : X -> Y) (f' : X' -> Y') (g : Y -> Z) (g' : Y' -> Z') : homot (funcomp (coprodf f f') (coprodf g g')) (coprodf (funcomp f g) (funcomp f' g')). Proof. intros. intro xx'. induction xx' as [ x | x' ]. apply idpath. apply idpath. Defined.