Lemma iscontrhfiberl1 {X Y : UU} (f : X -> Y) (g : Y -> X) (efg: ∏ y : Y, f (g y) = y) (x0 : X) (is : iscontr (hfiber (g ∘ f) x0)) : iscontr (hfiber g x0). Proof. intros. set (f1 := hfibersgftog f g x0). set (g1 := λ (xe : hfiber g x0), pr1 (constr2 f g efg x0 xe)). set (efg1 := λ (xe : hfiber g x0), ! (pr2 (constr2 f g efg x0 xe))). apply (iscontrretract f1 g1 efg1). apply is. Defined.