{A B B' : Type} `{Indecomposable A} (h : A + B <~> A + B') : B <~> B'. Proof. pose (f := equiv_decompose (h o inl)). pose (g := equiv_decompose (h o inr)). pose (k := (h oE (f +E g))). pose (k' := k oE (equiv_sum_assoc _ _ _) oE ((equiv_sum_assoc _ _ _)^-1 +E 1) oE (1 +E (equiv_sum_symm _ _) +E 1) oE ((equiv_sum_assoc _ _ _) +E 1) oE (equiv_sum_assoc _ _ _)^-1). destruct (equiv_unfunctor_sum k' (fun x : decompose_l (h o inl) + decompose_l (h o inr) => match x as x0 return (is_inl (k' (inl x0))) with | inl x0 => x0.2 | inr x0 => x0.2 end) (fun x : decompose_r (h o inl) + decompose_r (h o inr) => match x as x0 return (is_inr (k' (inr x0))) with | inl x0 => x0.2 | inr x0 => x0.2 end)) as [s t]; clear k k'. refine (t oE (_ +E 1) oE g^-1). destruct (equiv_indecomposable_sum s^-1) as [[p q]|[p q]]; destruct (equiv_indecomposable_sum f^-1) as [[u v]|[u v]]. - refine (v oE q^-1). - elim (indecompose0 (v^-1 o p)). - refine (Empty_rec (indecompose0 _)); intros a. destruct (is_inl_or_is_inr (h (inl a))) as [l|r]. * exact (q^-1 (a;l)). * exact (v^-1 (a;r)). - refine (u oE p^-1). Defined.
Require Import HoTT.Basics. Require Import Types.Empty Types.Unit Types.Prod Types.Sigma. Require Import Types.Bool.