{A A' B B' : Type} (h : A + B <~> A' + B') (Ha : forall a:A, is_inl (h (inl a))) (Hb : forall b:B, is_inr (h (inr b))) : A <~> A' := Build_Equiv _ _ (unfunctor_sum_l h Ha) (isequiv_unfunctor_sum_l h Ha Hb). Global Instance isequiv_unfunctor_sum_r {A A' B B' : Type} (h : A + B <~> A' + B') (Ha : forall a:A, is_inl (h (inl a))) (Hb : forall b:B, is_inr (h (inr b))) : IsEquiv (unfunctor_sum_r h Hb). Proof. simple refine (isequiv_adjointify _ _ _ _). - refine (unfunctor_sum_r h^-1 _); intros b'. remember (h^-1 (inr b')) as x eqn:p. destruct x as [a|b]. + apply moveL_equiv_M in p. elim (p^ # (Ha a)). + exact tt. - intros b'. refine (unfunctor_sum_r_compose _ _ _ _ _ @ _). refine (path_sum_inr A' _). refine (unfunctor_sum_r_beta _ _ _ @ _). apply eisretr. - intros b. refine (unfunctor_sum_r_compose _ _ _ _ _ @ _). refine (path_sum_inr A _). refine (unfunctor_sum_r_beta (h^-1 o h) _ b @ _). apply eissect. Defined.
Require Import HoTT.Basics. Require Import Types.Empty Types.Unit Types.Prod Types.Sigma. Require Import Types.Bool.