{A B : Type} {Q : B -> Type} (f : A <~> B) : sig (Q o f) <~> sig Q := equiv_functor_sigma f (fun a => 1%equiv). Global Instance isequiv_pr1_contr {A} {P : A -> Type} `{forall a, Contr (P a)} : IsEquiv (@pr1 A P) | 100. Proof. refine (isequiv_adjointify (@pr1 A P) (fun a => (a ; center (P a))) _ _). - intros a; reflexivity. - intros [a p]. refine (path_sigma' P 1 (contr _)). Defined.
Require Import HoTT.Basics. Require Import Types.Arrow Types.Paths.