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