equiv_functor_sum' {A A' B B' : Type} (f : A <~> A') (g : B <~> B') : A + B <~> A' + B' := equiv_functor_sum (f := f) (g := g).
Require Import HoTT.Basics. Require Import Types.Empty Types.Unit Types.Prod Types.Sigma. Require Import Types.Bool.