fact: Definition functor_sum_homotopic {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'.
imports: HoTT.Basics Types.Empty Types.Unit Types.Prod Types.Sigma Types.Bool Types.Forall