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