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