Lemma weqhfpcomm {X X' Y : UU} (f : X -> Y) (f' : X' -> Y): hfp f f' ≃ hfp 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)))). apply (weqcomp w1 w2). Defined.