Theorem isweqhfiberfp {X Y : UU} (f : X -> Y) (P : Y -> UU) (yp : total2 P) : isweq (hfiberfpmap f P yp). Proof. intros. set (int1 := hfibersgftog (hffpmap2 f P) (λ u : (total2 (λ u : total2 P, hfiber f (pr1 u))), (pr1 u)) yp). assert (is1 : isweq int1). simpl in int1. apply (pr2 (weqhfibersgwtog (make_weq _ (isweqhff f P)) (λ u : total2 (λ u : total2 P, hfiber f (pr1 u)), pr1 u) yp)). set (phi := invezmappr1 (λ u : total2 P, hfiber f (pr1 u)) yp). assert (is2 : isweq phi). apply (pr2 (invweq (ezweqpr1 (λ u : total2 P, hfiber f (pr1 u)) yp))). apply (twooutof3c int1 phi is1 is2). Defined.