fact: 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')).
imports: UniMath.Foundations.Preamble