Definition weqfp {X Y : UU} (w : X ≃ Y) (P : Y -> UU) : (∑ x : X, P (w x)) ≃ (∑ y, P y). Proof. intros. exists (weqfp_map w P). refine (isweq_iso _ (weqfp_invmap w P) _ _). { intros xp. use total2_paths_f. { simpl. apply homotinvweqweq. } simpl. rewrite <- weq_transportf_adjointness. rewrite transport_f_f. rewrite pathsinv0l. apply idpath. } { intros yp. simple refine (total2_paths_f _ _). { simpl. apply homotweqinvweq. } simpl. rewrite transport_f_f. rewrite pathsinv0l. apply idpath. } Defined.