Corollary isweqmaponsec {X : UU} (P Q : X -> UU) (f : ∏ x, (P x) ≃ (Q x)) : isweq (maponsec _ _ f). Proof. intros. unfold isweq. intro y. assert (is1 : iscontr (∏ x, hfiber (f x) (y x))). { assert (is2 : ∏ x, iscontr (hfiber (f x) (y x))) by (intro x; apply ((pr2 (f x)) (y x))). apply funcontr. assumption. } apply (iscontrweqb (weqhfibertoforall P Q f y) is1). Defined.