{A B : Type} (z z' : A + B) := Build_Equiv _ _ _ (@isequiv_path_sum A B z z'). Global Instance ishprop_hfiber_inl {A B : Type} (z : A + B) : IsHProp (hfiber inl z). Proof. destruct z as [a|b]; unfold hfiber. - refine (istrunc_equiv_istrunc _ (equiv_functor_sigma_id (fun x => (inl x) (inl a)))). - refine (istrunc_isequiv_istrunc _ (fun xp => inl_ne_inr (xp.1) b xp.2)^-1). Defined.
Require Import HoTT.Basics. Require Import Types.Empty Types.Unit Types.Prod Types.Sigma. Require Import Types.Bool.