Corollary isweqfpmap {X Y : UU} (w : X ≃ Y)(P : Y -> UU) : isweq (fpmap w P). Proof. intros. unfold isweq. intro y. set (h := hfiberfpmap w P y). assert (X1 : isweq h). apply isweqhfiberfp. assert (is : iscontr (hfiber w (pr1 y))). apply (pr2 w). apply (iscontrweqb (make_weq h X1) is). Defined.