trunc_sum' n A B `{IsTrunc n Bool, IsTrunc n A, IsTrunc n B} : (IsTrunc n (A + B)). Proof. eapply istrunc_equiv_istrunc; [ esplit; exact (@isequiv_sum_of_sig _ _) | ]. typeclasses eauto. Defined.
Require Import HoTT.Basics. Require Import Types.Empty Types.Unit Types.Prod Types.Sigma. Require Import Types.Bool.