A <~> {x:A & P x} + {x:A & ~(P x)}. Proof. transparent assert (f : (A -> {x:A & P x} + {x:A & ~(P x)})). { intros x. destruct (dec (P x)) as [p|np]. - exact (inl (x;p)). - exact (inr (x;np)). } refine (Build_Equiv _ _ f _). refine (isequiv_adjointify _ (fun z => match z with | inl (x;p) => x | inr (x;np) => x end) _ _). - intros [[x p]|[x np]]; unfold f; destruct (dec (P x)) as [p'|np']. + apply ap, ap, path_ishprop. + elim (np' p). + elim (np p'). + apply ap, ap, path_ishprop. - intros x; unfold f. destruct (dec (P x)); cbn; reflexivity. Defined.
Require Import HoTT.Basics. Require Import Types.Empty Types.Unit Types.Prod Types.Sigma. Require Import Types.Bool.