Lemma weqhfibertobhfiber {X Y : UU} (f : X -> Y) (y : Y) (is : isisolated Y y) : (hfiber f y) ≃ (bhfiber f y is). Proof. intros. set (g := eqbx Y y is). set (ye := pr1 (iscontrhfibereqbx Y y is)). split with (hfibersftogf f g true ye). apply (isofhlevelfffromZ 0 _ _ ye (fibseqhf f g true ye)). apply (isapropifcontr). apply (iscontrhfibereqbx _ y is). Defined.