Definition hffpmap2 {X Y : UU} (f : X -> Y) (P : Y -> UU) : (∑ x, P (f x)) -> ∑ u : total2 P, hfiber f (pr1 u). Proof. intros X0. set (u:= fpmap f P X0). split with u. set (x:= pr1 X0). split with x. simpl. apply idpath. Defined.