Theorem weqhfibershomot {X Y : UU} (f g : X -> Y) (h : f ~ g) (y : Y) : hfiber f y ≃ hfiber g y. Proof. intros. set (ff := hfibershomotftog f g h y). set (gg := hfibershomotgtof f g h y). split with ff. assert (effgg : ∏ xe : _, ff (gg xe) = xe). { intro xe. induction xe as [x e]. simpl. assert (eee : ! h x @ h x @ e = maponpaths g (idpath x) @ e). { simpl. induction e. induction (h x). apply idpath. } set (xe1 := make_hfiber g x (! h x @ h x @ e)). set (xe2 := make_hfiber g x e). apply (hfibertriangle2 g xe1 xe2 (idpath x) eee). } assert (eggff : ∏ xe : _, gg (ff xe) = xe). { intro xe. induction xe as [x e]. simpl. assert (eee : h x @ !h x @ e = maponpaths f (idpath x) @ e). { simpl. induction e. induction (h x). apply idpath. } set (xe1 := make_hfiber f x (h x @ ! h x @ e)). set (xe2 := make_hfiber f x e). apply (hfibertriangle2 f xe1 xe2 (idpath x) eee). } apply (isweq_iso _ _ eggff effgg). Defined.