{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))) (b' : B') : hfiber (unfunctor_sum_r h Hb) b' <~> hfiber h (inr b'). Proof. simple refine (equiv_adjointify _ _ _ _). - intros [b p]. exists (inr b). refine (_ @ ap inr p). symmetry; apply inr_un_inr. - intros [[a|b] p]. + specialize (Ha a). abstract (rewrite p in Ha; elim Ha). + exists b. apply path_sum_inr with A'. refine (_ @ p). apply inr_un_inr. - intros [[a|b] p]; simpl. + apply Empty_rec. specialize (Ha a). abstract (rewrite p in Ha; elim Ha). + apply ap. apply moveR_Vp. exact (eisretr (@path_sum A' B' _ _) (inr_un_inr (h (inr b)) (Hb b) @ p)). - intros [b p]. apply ap. rewrite concat_p_Vp. pose (@isequiv_path_sum A' B' (inr (unfunctor_sum_r h Hb b)) (inr b')). exact (eissect (@path_sum A' B' (inr (unfunctor_sum_r h Hb b)) (inr b')) p). Defined.
Require Import HoTT.Basics. Require Import Types.Empty Types.Unit Types.Prod Types.Sigma. Require Import Types.Bool.