{A B C} (f : C -> A + B) : decompose_l f + decompose_r f <~> C. Proof. simple refine (equiv_adjointify (sum_ind (fun _ => C) pr1 pr1) _ _ _). - intros c; destruct (is_inl_or_is_inr (f c)); [ left | right ]; exists c; assumption. - intros c; destruct (is_inl_or_is_inr (f c)); reflexivity. - intros [[c l]|[c r]]; simpl; destruct (is_inl_or_is_inr (f c)). + apply ap, ap, path_ishprop. + elim (not_is_inl_and_inr' _ l i). + elim (not_is_inl_and_inr' _ i r). + apply ap, ap, path_ishprop. Defined.
Require Import HoTT.Basics. Require Import Types.Empty Types.Unit Types.Prod Types.Sigma. Require Import Types.Bool.