{A A' B B' : Type} {f f' : A -> A'} {g g' : B -> B'} (p : f == f') (q : g == g') : functor_sum f g == functor_sum f' g'. Proof. intros [a|b]. - exact (ap inl (p a)). - exact (ap inr (q b)). Defined.
Require Import HoTT.Basics. Require Import Types.Empty Types.Unit Types.Prod Types.Sigma. Require Import Types.Bool.