fact: Definition equiv_pr1 {A : Type} (P : A -> Type) `{forall x, Contr (P x)} : { x : A & P x } <~> A := Build_Equiv _ _ (@pr1 A P) _.
imports: Basics.Overture Basics.PathGroupoids Basics.Contractible Basics.Tactics