{A B} (P : A + B -> Type) (fg : (forall a, P (inl a)) * (forall b, P (inr b))) : forall s, P s := @sum_ind A B P (fst fg) (snd fg). Global Instance isequiv_sum_ind `{Funext} `(P : A + B -> Type) : IsEquiv ( P) | 0. Proof. apply (isequiv_adjointify ( P) (fun f => (fun a => f (inl a), fun b => f (inr b)))); repeat ((exact idpath) || intros [] || intro || apply path_forall). Defined.
Require Import HoTT.Basics. Require Import Types.Empty Types.Unit Types.Prod Types.Sigma. Require Import Types.Bool.