fact: Definition equiv_functor_sum `{IsEquiv A A' f} `{IsEquiv B B' g} : A + B <~> A' + B' := Build_Equiv _ _ (functor_sum f g) _.
imports: HoTT.Basics Types.Empty Types.Unit Types.Prod Types.Sigma Types.Bool Types.Forall