Lemma constr2 {X Y : UU} (f : X -> Y) (g : Y -> X) (efg: ∏ y : Y, f (g y) = y) (x0 : X) (xe : hfiber g x0) : ∑ xe' : hfiber (g ∘ f) x0, xe = hfibersgftog f g x0 xe'. Proof. intros. induction xe as [y0 e]. set (eint := pathssec1 _ _ efg _ _ e). set (ee := ! (maponpaths g eint) @ e). split with (make_hfiber (g ∘ f) x0 ee). unfold hfibersgftog. unfold make_hfiber. simpl. apply (two_arg_paths_f eint). induction eint. apply idpath. Defined.