Lemma isweqhff {X Y : UU} (f : X -> Y) (P : Y -> UU) : isweq (hffpmap2 f P). Proof. intros. set (int := total2 (λ x : X, total2 (λ u : coconusfromt Y (f x), P (pr1 u)))). set (intpair := tpair (λ x:X, total2 (λ u : coconusfromt Y (f x), P (pr1 u)))). set (toint := λ z : (total2 (λ u : total2 P, hfiber f (pr1 u))), intpair (pr1 (pr2 z)) (tpair (fun u: coconusfromt Y (f (pr1 (pr2 z))) => P (pr1 u)) (coconusfromtpair _ (pr2 (pr2 z))) (pr2 (pr1 z)))). set (fromint := λ z : int, tpair (λ u : total2 P, hfiber f (pr1 u)) (tpair P (pr1 (pr1 (pr2 z))) (pr2 (pr2 z))) (make_hfiber f (pr1 z) (pr2 (pr1 (pr2 z))))). assert (fromto : ∏ u : (total2 (λ u : total2 P, hfiber f (pr1 u))), (fromint (toint u)) = u). simpl in toint. simpl in fromint. simpl. intro u. induction u as [ t x ]. induction x. induction t as [ p0 p1 ]. simpl. unfold toint. unfold fromint. simpl. apply idpath. assert (tofrom : ∏ u : int, (toint (fromint u)) = u). intro. induction u as [ t x ]. induction x as [ t0 x ]. induction t0. simpl in x. simpl. unfold fromint. unfold toint. simpl. apply idpath. assert (is : isweq toint). apply (isweq_iso toint fromint fromto tofrom). clear tofrom. clear fromto. clear fromint. set (h := λ u : total2 (λ x : X, P (f x)), toint ((hffpmap2 f P) u)). simpl in h. assert (l1 : ∏ x : X, isweq (λ p: P (f x), tpair (λ u : coconusfromt _ (f x), P (pr1 u)) (coconusfromtpair _ (idpath (f x))) p)). intro. apply (centralfiber P (f x)). assert (X0 : isweq h). apply (isweqfibtototal (λ x : X, P (f x)) (λ x : X, total2 (λ u : coconusfromt _ (f x), P (pr1 u))) (λ x : X, make_weq _ (l1 x))). apply (twooutof3a (hffpmap2 f P) toint X0 is). Defined.