{B C} (f:C ->B) : C <~> {y:B & hfiber f y}. Proof. snrefine (Build_Equiv _ _ _ ( Build_IsEquiv C {y:B & {x:C & f x = y}} (fun c => (f c; (c; idpath))) (fun c => c.2.1) _ (fun c => idpath) _)). - intros [? [? []]]; reflexivity. - reflexivity. Defined.
Require Import Basics Types Diagrams.CommutativeSquares HSet.