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