`{Funext} (A B C : Type) : (A -> C) * (B -> C) <~> (A + B -> C) := equiv_sum_ind (fun _ => C). Global Instance istrunc_sum n' (n := n'.+2) `{IsTrunc n A, IsTrunc n B} : IsTrunc n (A + B) | 100. Proof. apply istrunc_S. intros a b. eapply istrunc_equiv_istrunc; [ exact (equiv_path_sum _ _) | ]. destruct a, b; exact _. Defined.
Require Import HoTT.Basics. Require Import Types.Empty Types.Unit Types.Prod Types.Sigma. Require Import Types.Bool.