(a' : A') : hfiber functor_sum (inl a') <~> hfiber f a'. Proof. simple refine (equiv_adjointify _ _ _ _). - intros [[a|b] p]. + exists a. exact (path_sum_inl _ p). + elim (inr_ne_inl _ _ p). - intros [a p]. exists (inl a). exact (ap inl p). - intros [a p]. apply ap. pose (@isequiv_path_sum A' B' (inl (f a)) (inl a')). exact (eissect (@path_sum A' B' (inl (f a)) (inl a')) p). - intros [[a|b] p]; simpl. + apply ap. pose (@isequiv_path_sum A' B' (inl (f a)) (inl a')). exact (eisretr (@path_sum A' B' (inl (f a)) (inl a')) p). + elim (inr_ne_inl _ _ p). Defined.
Require Import HoTT.Basics. Require Import Types.Empty Types.Unit Types.Prod Types.Sigma. Require Import Types.Bool.