Definition hfiberfpmap {X Y : UU} (f : X -> Y) (P : Y -> UU) (yp : total2 P) : hfiber (fpmap f P) yp -> hfiber f (pr1 yp). Proof. intros X0. set (int1:= hfibersgftog (hffpmap2 f P) (λ u : (∑ u : total2 P, hfiber f (pr1 u)), (pr1 u)) yp). set (phi := invezmappr1 (λ u:total2 P, hfiber f (pr1 u)) yp). apply (phi (int1 X0)). Defined.