Theorem isweqbandfmap {X Y : UU} (w : X ≃ Y) (P : X -> UU) (Q : Y -> UU) (fw : ∏ x : X, P x ≃ Q (w x)) : isweq (bandfmap _ P Q fw). Proof. intros. set (f1 := totalfun P _ fw). set (is1 := isweqfibtototal P (λ x:X, Q (w x)) fw). set (f2:= fpmap w Q). set (is2:= isweqfpmap w Q). assert (h: ∏ xp: total2 P, (f2 (f1 xp)) = (bandfmap w P Q fw xp)). { intro. apply idpath. } apply (isweqhomot _ _ h (twooutof3c f1 f2 is1 is2)). Defined.