Lemma weqhfibertohfp {X Y : UU} (f : X -> Y) (y : Y) : hfiber f y ≃ hfp (λ _:unit, y) f. Proof. intros. set (ff := hfibertohfp f y). set (gg := hfptohfiber f y). split with ff. assert (egf : ∏ xe : _, (gg (ff xe)) = xe). intro. induction xe. apply idpath. assert (efg : ∏ hf : _, (ff (gg hf)) = hf). intro. induction hf as [ tx e ]. induction tx as [ t x ]. induction t. apply idpath. apply (isweq_iso _ _ egf efg). Defined.