Definition weqhfiberunit {X Z : UU} (i : X -> Z) (z : Z) : (∑ x, hfiber (λ _ : unit, z) (i x)) ≃ hfiber i z. Proof. intros. use weq_iso. + intros [x [t e]]. exact (x,,!e). + intros [x e]. exact (x,,tt,,!e). + intros [x [t e]]. apply maponpaths. simple refine (two_arg_paths_f _ _). * apply isapropunit. * simpl. induction e. rewrite pathsinv0inv0. induction t. apply idpath. + intros [x e]. apply maponpaths. apply pathsinv0inv0. Defined.