fact: Definition equiv_sum_distributive `{Funext} (A B C : Type) : (A -> C) * (B -> C) <~> (A + B -> C) := equiv_sum_ind (fun _ => C).
imports: HoTT.Basics Types.Empty Types.Unit Types.Prod Types.Sigma Types.Bool Types.Forall