(a : A) (p : P a) : equiv_decidable_sum a = inl (a;p). Proof. unfold equiv_decidable_sum; cbn. destruct (dec (P a)) as [p'|np']. - apply ap, path_sigma_hprop; reflexivity. - elim (np' p). Defined.
Require Import HoTT.Basics. Require Import Types.Empty Types.Unit Types.Prod Types.Sigma. Require Import Types.Bool.