{X} (x : X) (P:X->Type) : P x <~> @hfiber (sig P) X pr1 x. Proof. snrefine (Build_Equiv _ _ _ (Build_IsEquiv (P x) { z : sig P & z.1 = x } (fun Px => ((x; Px); idpath)) (fun Px => transport P Px.2 Px.1.2) _ (fun Px => idpath) _)). - intros [[] []]; reflexivity. - reflexivity. Defined.
Require Import Basics Types Diagrams.CommutativeSquares HSet.