Definition homotcoprodfhomot {X X' Y Y' : UU} (f g : X -> Y) (f' g' : X' -> Y') (h : homot f g) (h' : homot f' g') : homot (coprodf f f') (coprodf g g') := λ xx' : _, match xx' with | ii1 x => maponpaths (@ii1 _ _) (h x) | ii2 x' => maponpaths (@ii2 _ _) (h' x') end.