Definition sumofmaps_homot {X Y Z : UU} {f f' : X → Z} {g g' : Y → Z} (h : f ~ f') (h2 : g ~ g') : sumofmaps f g ~ sumofmaps f' g'. Proof. intro x. induction x as [x|y]. - exact (h x). - exact (h2 y). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics.