Definition weqhfptohfpoverX' {X X' Y : UU} (f : X -> Y) (f' : X' -> Y) : hfp f f' ≃ hfpoverX' f f'. Proof. intros. set (w1 := weqfp (weqdirprodcomm X X') (λ xx' : X' × X , (f' (pr1 xx')) = (f (pr2 xx')))). simpl in w1. set (w2 := weqfibtototal (λ x'x : X' × X, (f' (pr1 x'x)) = (f (pr2 x'x))) (λ x'x : X' × X, (f (pr2 x'x)) = (f' (pr1 x'x))) (λ x'x : _, weqpathsinv0 (f' (pr1 x'x)) (f (pr2 x'x)))). set (w3 := weqtotal2asstor (λ x' : X', X) (λ x'x : X' × X, (f (pr2 x'x)) = (f' (pr1 x'x)))). simpl in w3. apply (weqcomp (weqcomp w1 w2) w3). Defined.